[Logiweb] ''peano empty'' not caught

[Martin Røpcke]

On Thu, 30 Jun 2005, Klaus Ebbe Grue wrote:

> Hi Martin,
>
>> I compiled and had the following in one of my proofs:
>> 
>> peano imply
>> 	peano x peano succ peano plus peano
>> peano is
>> 
>> there should have been a "y" at the end of the second line. Shouldn't 
>> "peano 'empty'" get caught as a syntax error by pyk? It compiled well but 
>> failed, of course, translating to something like:
>> 
>> ...[ x' + peano ]...
>
> I guess the explanation is that you have a construct named "peano". It could 
> well be the name of the page ("PAGE peano" introduces a construct named 
> "peano" which can be used in formulas just like any other construct). And it 
> is typically renderede something like "peano" (e.g. by defining the pyk 
> aspect of "peano" to be "peano" and defining no tex aspect).
>
> But there can be other explanations as well, e.g. that there is a construct 
> named "* peano peano is *", but the explanation above also explains the ...[ 
> x' + peano ]...

I see, I didn't think of my references, but it makes sense to me now. 
Thank you.

Regards,
Martin