The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

I come back to this question after some thinking about it.

Indeed uconstr does not fit in the suggestion I made. Something you
may be able to do in some cases (but not in your case I guess, see
below) is to use the String type where you need some specific non
typable format.

Inductive args :=
  Step: args
| Iter: nat -> args
| Hyp: forall (A:Type) (t:A), args
| Trans: String -> args.   (* <--- here *)

and hopefully you can analyse the string character by character to
implement the behaviour you want.

BUT it seems your uconstr has subparts that you want to consider as
real coq terms, and I am not aware of a way to take a String and
transform it into a constr by giving it to the  coq parser.

What are the possible forms of your uconstr arguments? Maybe you can
describe them in a inductive type.

Best,
Pierre




2017-10-30 14:25 GMT+01:00 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
>>
>