Logiweb(TM)

14.261 At-seqop used on non-quantifier

Prev Up Next Page 732 of 800 Search internet


Origin: check. Landing-place: diagnose.

At-seqop used on non-quantifier: R

The At sequent operator applied to a sequent << P ,, C ,, All #x : A >> and a metaterm y yields << P ,, C ,, B >> where B is the result of replacing #x by y in A. The 'At-seqop used on non-quantifier' indicates that the conclusion of the sequent did not have form All #x : A. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 732 of 800 Search logiweb.eu

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