Page 743 of 800
| Page 743 of 800 | Search internet |
Origin: check. Landing-place: diagnose.
The proof of L does not prove what the lemma says. After macro expansion, the lemma says: A
After macro, tactic, and sequent expansion, the proof concludes: B
The sequent evaluator has found a lemma named L and a proof of Lemma L but the proof did not prove that right thing. The error message indicates what the lemma says and what the proof proves. Both statements may be difficult to read since the message states what the lemma says and what the proof proves after macro expansion. In particular, if a lemma states that e.g. 
holds in Peano arithmetic before macro expansion then the lemma says 
after macro expansion.
| Page 743 of 800 | Search logiweb.eu |