Re: [ProofPower] Schema in a predicate stub

2011-07-11 Thread Rob Arthan
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 ==

Re: [ProofPower] Schema in a predicate stub

2011-07-11 Thread Phil Clayton
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

[ProofPower] Schema in a predicate stub

2011-06-21 Thread Phil Clayton
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