Thibaut Pérami (Sep 03 2024 at 12:24): Thibaut Pérami (Sep 03 2024 at 12:24):Hi all, I was wondering if there was a way to make an antiquotation to include an ident in a constr similar to $x for including a constr variable in another galina expression.
For example imagine I have an identifier n : nat in my goal context and a Ltac2 variable h : ident that contains that identifier n. I want to create the term n + n using h. I didn't find any combination of short antiquotations to do it. The only solution is let hn := Control.hyp h in '($hn + $hn).
Is there a shorter way?
Janno (Sep 03 2024 at 12:56):I am not aware of anything like that. There is &h but unfortunately that stands for Control.hyp @h instead of Control.hyp h.
Last updated: Oct 12 2024 at 13:01 UTC