[Logiweb] Re: * proof of * reads * (fwd)

[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
> compiling definitions
> 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
>


_______________________________________________
Logiweb mailing list
Logiweb at diku.dk
http://miming.diku.dk/mailman/listinfo/logiweb
(Web access from inside DIKUs LAN only)