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
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to