Logiweb(TM)

14.272 The proof does not prove what the lemma says

Prev Up Next 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. x + y = y + x holds in Peano arithmetic before macro expansion then the lemma says PA infer x + y = y + x after macro expansion.

Prev Up Next Page 743 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05