Open Lysxia opened 4 years ago
The problem is tactics are currently only highlighted when they're in a coqProofBody
region, which looks for a starting delimiter like Proof
or Next Obligation
. Without that it's tricky to tell when a proof starts. Some options I can think of are:
Lemma
, or Theorem
, etc. It should probably also check that it's not defined in that same command (Example a : True := I.
), but this also has some corner cases (Instance x : Reflexive R := _.
).1 or 3 are the easiest options but I'm open to 2 if you think this is a common enough/idiomatic use case.
Somewhat related: #43.
I'm fine with not fixing it if it's not easy. I just wanted to mention it because it seems somewhat common, but I'm not at all fond of that style.
When I next get some time I'll experiment with how hard it is to make a best-effort attempt at something like option 2.
As if living with the rooster was not hard enough already,
some proofs in the standard library start with both
Next Obligation
and Proof
and thus manifest this issue.
The following excerpt is from theories/Classes/EquivDec.v
.
#[global]
Program Instance unit_eqdec : EqDec unit eq := fun x y => in_left.
Next Obligation.
Proof.
do 2 match goal with [ x : () |- _ ] => destruct x end.
reflexivity.
Qed.
Compare how
cbn
is highlighted in this example: