Require Import Ltac2.Ltac2.
Goal 1 + 1 = 2.
Set Default Proof Mode "Classic".
ltac2:(lia2).
fails with 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