Stream: Coq users

Topic: open_constr


view this post on Zulip Ralf Jung (Nov 16 2020 at 15:49):

Is there any way to force ltac to parse a term as open_constr? Currently the only way I know to do this is

Tactic Notation "my_unify" open_constr(e1) open_constr(e2) :=
  unify e1 e2.

but that is kind of silly...

view this post on Zulip Ralf Jung (Nov 16 2020 at 15:52):

I tried unify e open_constr:(<pattern goes here>) but that does not work... the docs seem to indicate uconstr should maybe work (is that the same as open_constr?), but uconstr:(...) keeps saying "Error: Syntax error: ')' expected after [ltac_expr level 5] (in [tactic_value])."

view this post on Zulip Ralf Jung (Nov 16 2020 at 15:53):

I can fix that strange syntax error with another layer of parentheses, but then the tactic still fails, whereas it works with my_unify...

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 16:06):

You have to create a trivial cut: let t := open_constr:(_) in unify t True.

view this post on Zulip Pierre-Marie Pédrot (Nov 16 2020 at 16:07):

uconstr is something else, it corresponds to an untyped syntax (essentially glob_constr in the ML nomenclature) that can be type-checked on the fly

view this post on Zulip Ralf Jung (Nov 16 2020 at 16:14):

Pierre-Marie Pédrot said:

You have to create a trivial cut: let t := open_constr:(_) in unify t True.

oh I see... I might keep the notation then actually, that is easier to read. thanks!


Last updated: Jan 31 2023 at 12:01 UTC