Next: ref-sem-ctr-dol, Previous: ref-sem-ctr-ite, Up: ref-sem-ctr [Contents][Index]
The following construct provides a kind of pseudo-negation meaning “P is not provable”. This is not real negation (“P is false”). The following two goals are equivalent:
\+ P (P -> fail ; true)