The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Pierre,

Thx for the suggestion but there is a problem with
the untyped argument <uconstr> which cannot be represented
as a Coq typed term.

Is there no way or extension for Tactic to manipulate
text ?

Dominique

Le 30/10/2017 à 12:03, Pierre Courtieu a écrit :
> 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
> <mailto: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
>