14.257 Uncurry-seqop used on unfit argument

Prev Up Next Page 728 of 800 Search internet

Origin: check. Landing-place: diagnose.

Uncurry-seqop used on unfit argument: R

The Uncurry sequent operator applied to a sequent << P ,, C ,, x infer ( y infer z ) >> yields << P ,, C ,, ( x oplus y ) infer z >> where x oplus y is meta-conjunction and u infer v is meta-implication. The 'Uncurry-seqop used on unfit argument' indicates that the conclusion of the sequent did not have form x infer ( y infer z ). The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 728 of 800 Search logiweb.eu

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