[Logiweb] ''peano empty'' not caught

[Klaus Ebbe Grue]

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 ]...

Klaus