Stream: math-comp devs

Topic: Typo handling in `rewrite` with `?`

Pierre Jouvelot (May 01 2022 at 20:01):

I understand why the following code works:

From mathcomp Require Import all_ssreflect.

Lemma foo n : n + 0 = n.
Proof.
Fail rewrite adddn0.
by rewrite 1?adddn0 addn0.
Qed.

but it seems to me that completing a proof mentioning a non-existing lemma (e.g., due to a typo in the name) only because it is "protected" by the? multiplier is somewhat unsatisfying. It seems a bit like allowing syntactically incorrect pieces of code in a program, as long as they are located in an unreachable part of the software.

Is there a way to trap this type of errors?

Last updated: Oct 13 2024 at 01:02 UTC