[Logiweb] * proof of * reads *

[Klaus Ebbe Grue]

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

The error message should mean that "* cut *" was defined on two distinct 
pages. Defining the same construct on two pages is ok, but using it 
afterwards gives an error message (the idea is that defining a "* cut *" 
both on a "base" page and an "xyzzy" page allows to refer to the two as "* 
base cut *" and "* xyzzy cut *").

It is strange, though that the pyk compiler seems to confuse symbol 85 of 
page 2 with *itself*.

Could you give me a pointer to your source text so that I can try to 
reproduce the error?

By the way:  "* cut *" is post-associative on the "base" page, so it also 
has to be post-associative on all referencing pages.

Klaus