Stream: Coq users

Topic: Make global definitions with Ltac

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?

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.

James Wood (May 05 2022 at 10:40):

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

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

James Wood (May 05 2022 at 10:45):

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

Gaëtan Gilbert (May 05 2022 at 10:54):

using templatecoq I guess

Paolo Giarrusso (May 05 2022 at 20:31):

Or coq-elpi nowadays

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: Oct 13 2024 at 01:02 UTC