Stream: Ltac2

Topic: Evar in Ltac2


view this post on Zulip 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)?

view this post on Zulip 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

view this post on Zulip Janno (Feb 01 2022 at 15:10):

The thread was about performance but it still shows at least one way of creating an evar :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Janno (Feb 02 2022 at 09:16):

Oh, yeah, I had forgotten to mention that. You can also call cbv with just beta on it, IIRC.

view this post on Zulip Janno (Feb 02 2022 at 09:16):

But your solution is the best solution, AFAIK


Last updated: Jan 31 2023 at 10:01 UTC