The "unused unfold" warning currently fires when it is not used in at least one branch of a multi-branch rewrite/intro-pattern. We could recover warning-free proofs for the standard library and examples, but this is not reasonable for larger proofs. Before turning it into an error, we need to tighten it.
The idea is to make the warning sentence-level: if a sentence contains an unfold that is not used in any part of the sentence, then the warning fires.
The "unused unfold" warning currently fires when it is not used in at least one branch of a multi-branch rewrite/intro-pattern. We could recover warning-free proofs for the standard library and examples, but this is not reasonable for larger proofs. Before turning it into an error, we need to tighten it.
The idea is to make the warning sentence-level: if a sentence contains an unfold that is not used in any part of the sentence, then the warning fires.