Is there any reason why a schema argument in a predicate stub (_?) isn't implicitly converted to a predicate?

A Z specification taking a Standard-compatible approach to booleans may have:


BOOL == P []
True == [| true]
False == [| false]

  if True then X else Y

However, this produces a type error: we must explicitly say that True is to be taken as a predicate, i.e.

  if %Pi% True then X else Y

which seems unnecessary.  Above example attached.

Phil

Attachment: schema_in_pred_stub.sml.gz
Description: GNU Zip compressed data

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to