14.256 Curry-seqop used on unfit argument

Prev Up Next Page 727 of 800 Search internet

Origin: check. Landing-place: diagnose.

Curry-seqop used on unfit argument: R

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

Prev Up Next Page 727 of 800 Search logiweb.eu

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