[Logiweb] Re: * proof of * reads *

[Kasper H0st Frederiksen]

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
Load: compiling definitions
Load: macro expanding

*** - Program stack overflow. RESET


-Kasper Frederiksen

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?


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

> I have found out that in order to compile the following bit of proof:
> ---
> "[ math khf theory proof of khf lemma one reads
> 	arbitrary meta a cut meta a
>   end math ]"
> ---
>
> ... I need to declare "PREASSOCIATIVE check: * proof of * reads *" in my 
> bibliography. It is strange then that i _don't_ need to declare
> "PREASSOCIATIVE check: arbitrary * cut *", infact if I add this line to my 
> bibliography i get the error:
>
> Frontend: parsing body
> Symbol 85 of page 2 has the same name as symbol 85 of page 2
> ---
>
> ---
> arbitrary meta a cut meta a
> ---
> File page.pyk line 222 char 2:
> Use of ambiguous construct
> Submission aborted
>
>
> Perhaps somone would lilke to comment on this.
>
> -Kasper Frederiksen
>