Mathis Bouverot-Dupuis (Jul 11 2024 at 11:46): Mathis Bouverot-Dupuis (Jul 11 2024 at 11:46):Hi all, in Ltac2 I would like to do the following : create a fresh evar with a given type and a given name.
I have tried epose (_ : $mytype) as $myname, but this is not exactly what I want : it adds the evar in the local context under the name myname (which I don't need), and the actual name of the evar (which is displayed to the user) is generated automatically based on mytype.
Is there a way to do what I want ?
Karl Palmskog (Jul 11 2024 at 11:47):this looks like a pure Ltac2 question to me
Notification Bot (Jul 11 2024 at 11:47):This topic was moved here from #Coq devs & plugin devs > Create a fresh evar using Ltac2 by Karl Palmskog.
Mathis Bouverot-Dupuis (Jul 11 2024 at 11:47):Karl Palmskog said:
this looks like a pure Ltac2 question to me
Indeed, sorry for the wrong channel.
Karl Palmskog (Jul 11 2024 at 11:48):no problem, this is how we handle channel discovery
Janno (Jul 11 2024 at 11:54):I don't think there is an API for this yet. An relatively easy option is open_constr:(_ : type) and running Std.eval_lazy { rBeta := true ; <everything else false> } on that to get rid of the cast. (You can also inspect the resulting term and strip off the Cast constructor).
Mathis Bouverot-Dupuis (Jul 11 2024 at 11:55):At the moment I use hnf on the result to get rid of the cast, but my main issue is that I can't control the name of the evar. Maybe someone knows of a hack to choose the name ?
Last updated: Oct 12 2024 at 13:01 UTC