coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Macro for Ltac

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Macro for Ltac
Date: Mon, 30 Oct 2017 11:03:48 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f51.google.com
Ironport-phdr: 9a23:FHqaNhV0tEZ8dPc8xLC+ctqT4xTV8LGtZVwlr6E/grcLSJyIuqrYZRKDt8tkgFKBZ4jH8fUM07OQ6P+wHzFYqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aSV3DMl9+If2wEYrPhey20fqz8tvdeVZmnj24NItzIQ+soE36sdQMnYpvN+5l0hrEuGFFPe9R2Hl0JF+Otxn578a0upVk9nID6Loa68dcXPCiLOwDRrtCAWF+Pg==

Hi,

I guess you should define a tactic taking a list (coq lists) over some inductive type describing the steps. Then some Tactic notation could get you close to the syntax you want.

Pierre

Le lun. 30 oct. 2017 à 10:26, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> a écrit :

Dear all,

I am wondering if there is a way to define macros within the
tactic language.

For instance, consider that I have already defined
tactic notations such as:

wcbv step
wcbv iter <integer>
wcbv hyp
wcbv trans <uconstr>

Then I would like to be able to write

wcbv step, hyp, hyp, trans (t @ a), iter 2.

instead of

wcbv step; do 2 wcbv hyp; wcbv trans (t @ a); wcbv iter 2.

Can I do this using Ltac and Tactic Notation ?
Because it seems neither can input <text> as an
argument (like latex or metapost macros would do)

Thanks very much in advance for any hint

Dominique

[Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
- Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
  - Re: [Coq-Club] fun <-> forall, Robbert Krebbers, 10/26/2017
    - Re: [Coq-Club] fun <-> forall, Ralf Jung, 10/26/2017
      - Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Burak Ekici, 10/26/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/26/2017
        Message not available
        Re: [Coq-Club] fun <-> forall, Samuel Gruetter, 10/28/2017
        [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
        Re: [Coq-Club] Macro for Ltac, Pierre Courtieu, 10/30/2017
        Re: [Coq-Club] Macro for Ltac, Dominique Larchey-Wendling, 10/30/2017
        
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/30/2017
        
        Re: [Coq-Club] fun <-> forall, Jason Gross, 10/31/2017
        Re: [Coq-Club] fun <-> forall, Clément Pit-Claudel, 10/31/2017
        
        Re: [Coq-Club] fun <-> forall, Cyril Cohen, 10/31/2017
    - Re: [Coq-Club] fun <-> forall, Anton Trunov, 10/26/2017