Phil,
On 6 Jul 2011, at 16:15, Phil Clayton wrote:
On 21/06/11 16:58, Phil Clayton wrote:
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 ==
Rob,
On 11/07/11 13:37, Rob Arthan wrote:
Further to my earlier reply to Phil's suggestion (outlined below), I
have looked into implementing it and it all looks good to me.
That's good - I was poised to have a go myself!
There is
only one consequence that I can see that looks a little
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