|Page 731 of 800||Search internet|
Origin: check. Landing-place: diagnose.
At-seqop used on non-meta-term: x
The At sequent operator applied to a sequent and a metaterm y yields where B is the result of replacing by y in A. The 'At-seqop used on non-meta-term' indicates that y was illformed. The error may indicate an error in the proof or a bug in a tactic.
|Page 731 of 800||Search logiweb.eu|