Stream: Ltac2

Topic: ✔ Create a fresh evar using Ltac2

Janno (Jul 11 2024 at 12:04):

Is the name static? You could try open_constr:(?[name] : type)

Janno (Jul 11 2024 at 12:05):

If not you can construct an identity function in Ltac2 with the right name (and type) and use open_constr:(my_lambda _)

Gaëtan Gilbert (Jul 11 2024 at 12:07):

you can avoid producing a cast in the term by using open_constr:(_ :> type), then no need to reduce it away

Mathis Bouverot-Dupuis (Jul 11 2024 at 12:10):

Gaëtan Gilbert said:

you can avoid producing a cast in the term by using open_constr:(_ :> type), then no need to reduce it away

Thanks for the trick !

Mathis Bouverot-Dupuis (Jul 11 2024 at 12:12):

Janno said:

If not you can construct an identity function in Ltac2 with the right name (and type) and use open_constr:(my_lambda _)

In my case the name is not static. I must admit the way the name of the evar is chosen is a bit obscur ; I (wrongly) assumed it depended only on the type of the evar. Anyways your solution works, thanks !

Notification Bot (Jul 11 2024 at 12:12):

Mathis Bouverot-Dupuis has marked this topic as resolved.

Last updated: Oct 12 2024 at 12:01 UTC