Ralf Jung (Nov 16 2020 at 15:49): 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...
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])."
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...
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.
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
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: Oct 03 2023 at 02:34 UTC