14.251 Init-seqop used on non-meta term

Prev Up Next Page 722 of 800 Search internet

Origin: check. Landing-place: diagnose.

Init-seqop used on non-meta term: x

The Init sequent operator applied to a term x yields the sequent << {{ x }} ,, {{}} ,, x >> which states that x is provable if x is provable. The operation requires x to be wellformed. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 722 of 800 Search logiweb.eu

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