Further to my earlier reply to Phil's suggestion (outlined below), I have looked into implementing it and it all looks good to me. There is only one consequence that I can see that looks a little strange at first, but makes sense when you think about it. This is the treatment of conditionals in quotations. If you enter:
%SZT% if 1 = 2 then 3 else 4 %>% it will fail, because the top level of a Z quotation is a predicate context (but not an operand of a stub, so non-predicates are allowed). To get this to work you have to force an expression context: %SZT% (if 1 = 2 then 3 else 4) %bigcolon% %bbU %>% Arguably we should have a separate quotation symbol to introduce a Z expression. The justification for the quotation to default to predicate is easy to see when you think about entering ordinary logical expressions: it would be very painful if they defaulted to being treated as schema expressions. I think the above slight complication (which is specific to conditionals or user-defined things like them) is worth the improved uniformity of the new approach. Regards, Rob. On 11 Jul 2011, at 09:45, Rob Arthan wrote: > 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? ... >>> > >> There is also the question of whether context stubs (_!) should be checked >> as predicates when the context is a predicate. Given >> >> function (op2 _!) >> >> would we expect >> >> %SZT% [ | op2 2] %>% >> >> to fail because 2 is not a predicate? (Irrespective of any definition op2 >> may have.) I think I would. (This looks more effort to implement.) > > > I will look into implementing something along these lines. > > Regards, > > Rob. > > > _______________________________________________ > Proofpower mailing list > [email protected] > http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
