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.


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

Proofpower mailing list

Reply via email to