The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Fri, 22 Jan 2010 11:16:47 +0100, Chantal Keller  
<chantal.keller AT wanadoo.fr> a écrit:

> Hello,
>
> Is it possible to define a conversion tactic [1] that could be used with  
> Eval? It can be useful to combine unfold, simpl...
>
> For instance:
>
> Ltac foo := unfold bar; simpl.
> Eval foo in foobar.
>
> Thanks,
> Chantal.
>
> [1]  
> http://coq.inria.fr/refman/Reference-Manual011.html#Conversion-tactics

that is not really a solution, but you can do:

Eval cbv beta iota zeta delta [bar] in foobar.

I never programmed any conversion tactic, but I think it is possible to do  
it in caml.
I believe that there is no conversion tactic aliasing, but it could be a  
feature,
and it is easy to implement.

As conversions may have a special status, not to add new constructions,
a rather clean hack may be to allow this kind of programmation:


"Definition bar := nat.

(*Ltac foo := cbv delta [bar].*)
Tactic Notation "'foo'" := (cbv delta [bar]).

Eval foo in bar."

So that foo is just unfolded and behaves like:


"Definition bar := nat.

Eval cbv delta [bar] in bar."



--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay