Stream: math-comp devs

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

view this post on Zulip 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.
Fail rewrite adddn0.
by rewrite 1?adddn0 addn0.

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: May 18 2024 at 08:40 UTC