Stream: Coq users

Topic: Make global definitions with Ltac


view this post on Zulip James Wood (May 05 2022 at 10:31):

I have an Ltac tactic which generates several closed terms. How can I bind those terms to global names, as if I had used Definition several times?

view this post on Zulip James Wood (May 05 2022 at 10:36):

To be concrete, say I have the following, and want to get x, y, and z out.

Ltac foo :=
  pose (x := Prop);
  pose (y := Set);
  pose (z := 4);
  idtac.

view this post on Zulip James Wood (May 05 2022 at 10:40):

They could also be let x := constr:(Prop) in ... &c; I don't mind.

view this post on Zulip Gaëtan Gilbert (May 05 2022 at 10:43):

something with abstract may work but is not recommended
tactics are not expected to modify the global environment

view this post on Zulip James Wood (May 05 2022 at 10:45):

Is there a more normal way of programmatically generating global definitions?

view this post on Zulip Gaëtan Gilbert (May 05 2022 at 10:54):

using templatecoq I guess

view this post on Zulip Paolo Giarrusso (May 05 2022 at 20:31):

Or coq-elpi nowadays

view this post on Zulip James Wood (May 09 2022 at 12:14):

Paolo Giarrusso said:

Or coq-elpi nowadays

Just for interest, I'd dismissed coq-elpi for this job because I needed to bind terms that involve universe polymorphism. In fact, it was my first choice, and I'd assumed that because coq-elpi let me do it, standard Coq tools would too.


Last updated: Feb 04 2023 at 21:02 UTC