14.247 Substitution produces non-meta-term

Prev Up Next Page 718 of 800 Search internet

Origin: check. Landing-place: diagnose.

Substitution of x with v produces non-meta-term

As an example, substitution of #y by All #x : #x in 1 + #y yields the illformed metaterm 1 + All #x : #x. The error may indicate an error in the proof or a bug in a tactic.

Prev Up Next Page 718 of 800 Search logiweb.eu

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