Stream: Ltac2

Topic: Ltac2 quiz on `ltac2`

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:35):

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 :-).

view this post on Zulip Gaëtan Gilbert (Apr 16 2022 at 21:50):

does Set Default Proof Mode have an effect on open proofs?
also I don't think you can use the foo:() stuff at toplevel

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:51):

you're 50% right — this works:

Set Default Proof Mode "Classic".

Goal 1 + 1 = 2.
ltac2:(lia2).

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:55):

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

view this post on Zulip Paolo Giarrusso (Apr 16 2022 at 21:56):

(the emphasis in quote is mine)

Last updated: May 31 2023 at 04:01 UTC