The Coq mailing list

[Chantal Keller <chantal.keller AT wanadoo.fr>]

Thanks for your answer.

AUGER a écrit :
> Le Fri, 22 Jan 2010 11:16:47 +0100, Chantal Keller 
> <chantal.keller AT wanadoo.fr> a écrit:
>>
> > For instance:
> >
> > Ltac foo := unfold bar; simpl.
> > Eval foo in foobar.
> that is not really a solution, but you can do:
>
> Eval cbv beta iota zeta delta [bar] in foobar.

This would perhaps work in this particular example, but I would like to 
be able to make a succession of unfold and simpl. Moreover,

cbv beta iota zeta delta

would make too much computation.

> 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."

Yes, it would be nice to have facilities to define new conversions in Coq.

Chantal.