[ProofPower] Schema in a predicate stub

[Phil Clayton]

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

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

  if True then X else Y



  if %Pi% True then X else Y

which seems unnecessary.  Above example attached.

Phil

A Z specification taking a Standard-compatible approach to booleans may have: However, this produces a type error: we must explicitly say that True is to be taken as a predicate, i.e.

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