Guillaume Melquiond (Feb 01 2022 at 14:55): Guillaume Melquiond (Feb 01 2022 at 14:55):I am trying to see whether I could use Ltac2 in place of Ltac1 and I am a bit struggling to find suitable constructs. What is the idiomatic way of creating an evar of a given type in LTac2 (and potentially depending on the current proof context)?
Janno (Feb 01 2022 at 15:09):There was a bit of discussion about this in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Creating.20evars.20in.20Ltac2
Janno (Feb 01 2022 at 15:10):The thread was about performance but it still shows at least one way of creating an evar :)
Guillaume Melquiond (Feb 01 2022 at 15:14):Thanks. It did not occur to me that I could just use open_constr. I was desperately looking at Ltac2.Constr and failing to see anything remotely useful.
Guillaume Melquiond (Feb 01 2022 at 22:45):Actually, open_constr:(_:$t) does not work. Indeed, it does not create an evar; it creates a casted evar. So, I ended up using the following (ugly) code to create evars:
Ltac2 evar t :=
let u := open_constr:(_:$t) in
match Constr.Unsafe.kind u with
| Constr.Unsafe.Cast v _ _ => v
| _ => Control.throw Init.Assertion_failure
end.
Oh, yeah, I had forgotten to mention that. You can also call cbv with just beta on it, IIRC.
Janno (Feb 02 2022 at 09:16):But your solution is the best solution, AFAIK
Last updated: Oct 12 2024 at 13:01 UTC