The notation for
refine is defined as
Ltac2 Notation refine := Control.refine.
As a consequence, the syntax differs from plain Ltac, while most tactics try to have the same syntax in both Ltac1 and Ltac2.
Is there a reason it is not defined as follows?
Ltac2 Notation refine c(thunk(open_constr)) := Control.refine c.
exact is defined like that and I think it is a mistake to make Ltac2 code look like Ltac1. I prefer
refine '(my term) over
refine (my term). (As a consequence I never use
exact because it forces me to write
exact $x when I have already let-bound my term to
x. Which I almost always do anyway.)
I do see the inconsistency, though. I guess my suggested solution would be to fix
Yeah, in general Ltac1 has hardwired support for parsing argument constrs, but in retrospective it's a bad idea.
I agree that all constr-only Ltac2 functions shouldn't be declared through a notation.
But then you would not even be able to write
refine x. You would have to fall back to
refine (fun () => x), wouldn't you?
Notation != syntactic alias.
Syntactic aliases implicitly thunk their argument
but it doesn't require adding a parsing rule
so you write
refine 'x and it's expanded to
Control.refine (fun () => open_constr:(x))
Syntax is not modular so every time you add a parsing rule you break some code out there
How does that work? Is that type-directed? If you write
refine x, Coq checks the type of
x and if it is not of type
unit -> constr, it thunks it?
it's a phase that occurs before type-checking
it's just that some global definitions have a special status and are expanded syntactically
refine x systematically thunks its argument?
in practice it's what you want most of the time (hence the fundamental dilemma of Ltac1 between forced values and lazy tactics)
Sure, but with this "in practice" argument, I also always want to pass an open constr to
no, because that one is a different grammar
and it's not true
sometimes you want to pass an Ltac2 variable
When I say "I", I mean "I".
you never pass meta variables to refine?
you're free to add a notation if you want
but it shouldn't be exposed by default in Ltac2, that's it
the less parsing rules, the more modular
Why would I pass a meta-variable to refine? What does it even achieve?
Ltac foo := intro x; refine x?
(meta as in Ltac variable, not a Meta as in the AST)
No, I would certainly use
aha, but it doesn't use the same unification algo
also it's very bad for HO stuff
refine as an argument to a tactical is hell in Ltac1
And even if I were to use
refine here, I would never write
Ltac foo := let x := fresh in intro x; refine x. I would write
Ltac foo := refine (fun x => x).
whatever (and these two things are not equivalent)
you're free to add your own notations in your devs
but you'll have a hard time convincing me that we need more Ltac1-like crappy notations in Ltac2
You are absolutely right. That is why I will keep using
Last updated: Jun 10 2023 at 06:31 UTC