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: Dec 05 2023 at 11:01 UTC