Require Import Ltac2.Ltac2. Goal 1 + 1 = 2. Set Default Proof Mode "Classic". ltac2:(lia2).
Syntax error: [ltac_use_default] expected after [ltac2_expr] (in [ltac2_command]).. It took me far too long to understand why (even if I managed), so I'll pose this as a quiz :-).
does Set Default Proof Mode have an effect on open proofs?
also I don't think you can use the
foo:() stuff at toplevel
you're 50% right — this works:
Set Default Proof Mode "Classic". Goal 1 + 1 = 2. ltac2:(lia2).
and I'll admit, the docs are even correct:
This option selects the proof mode to use when starting a proof.
I'd still enjoy a custom error for
ltac2: in ltac2 mode, but we can't have everything
(the emphasis in quote is mine)
Last updated: Dec 01 2023 at 07:01 UTC