The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Jason --

There are several synonyms for a term that is being matched on in Ltac. I want to change them all to a single canonical term before running that Ltac so that my Ltac is more robust. This piece of code gets run a lot, so speed is very important.

On Fri, Mar 22, 2013 at 5:09 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Yes, I think I remember hearing that [change] is hacked together to some extent.  (For example, I think you can use question marks and holes in [change], but only if it's not inside of some other Ltac code.)

I think you could also do something like

Ltac foo x A B :=
  match x with
    | appcontext C[A] => let C' := context C[B] in
                                         foo C' A B
    | _ => x
  end.

which has the (debatable) advantage of not using continuations, but the disadvantage of using context (and of being recursive) which you said you didn't want.

What's the intended use case?

-Jason

On Mar 22, 2013 4:20 PM, "Gregory Malecha" <gmalecha AT eecs.harvard.edu> wrote:

That would work, it seems very heavy-handed though.

On Fri, Mar 22, 2013 at 3:07 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Can do something like (untested):

Ltac do_change x A B tac :=
let H := fresh in
pose x as H;
change A with B in x;
let x' := eval unfold H in H;
clear H;
tac x'.

?

-Jason

On Mar 22, 2013 2:18 PM, "Gregory Malecha" <gmalecha AT eecs.harvard.edu> wrote:

Hello --

Is there a way in Ltac to run [change] on a term? For example, I'd like to do:

let x := eval change A with B in x in ....

in order to change all of the uses of A with B.

Ideally I would be able to do this without a [match ... with context [ A ] => ... end].

Thanks.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/