[Logiweb] Re: * proof of * reads *

[Klaus Ebbe Grue]

On Mon, 30 May 2005, Kasper H0st Frederiksen wrote:

> And another thing. When i compile:
> ---
> "[ math khf theory proof of khf lemma one reads
> arbitrary meta a cut
> line meta a because meta a indeed meta a cut meta a
>   end math ]"
> ---
> ... i get the error:
>
> ITERATION 1
>> compiling definitions
>> macro expanding
>
> *** - Program stack overflow. RESET

It could be an error in the pyk compiler. Or it could be that macro 
expansion loops indefinitely. As an example, if you say
   macro define myconstruct as myconstruct end define
then myconstruct will macro expand indefinitely (or, rather, overflow the 
stack).

> ps. In responce to an erlyer post. Do we realy have to redefine Modus Ponens 
> on our own pages? Why can't we reference the MP rule on the check page?

Do you reference the *new* "check" page? The one at
   http://www.diku.dk/~grue/logiweb/20050502/home/grue/check/
   GRD-2005-05-26-UTC-06-49-32-964854/
with reference
   nani
   nete kuti kata neki sete  kaka sinu seke nune tasi
   tena tana tise kati sune  naki suki suni tise tatu
   ketu kuke susi sena seke  susu sise nasa natu

Klaus