[Logiweb] * proof of * reads *

[Martin Røpcke]

> You state in a number of e-mails that "* proof of * reads *" is defined on 
> the check page. But it is defined on the base page.
>
> To see this, do as follows:
> Look up the base page. Then navigate to Dictionary->Pyk. Then do a "search on 
> this page" for "* proof of * reads *". There you find a line saying
>  589 3 * proof of * reads *
> which indicates that symbol 589 of the base page has arity 3 and pyk name "* 
> proof of * reads *". That proves that the base page defines a "* proof of * 
> reads *" construct. Repeating the above for the check page reveals that the 
> check page defines no "* proof of * reads *" construct.

I suppose the fault is mine -- coming from posing questions when being too 
tired and not understanding things too well. I've looked in the 
ACTUAL SOURCE and found "* proof of * reads *" in both source files
(I see that now.) I probably found it first in check page 
and then the "...end proof" construct on base page got me fooled.

> I am not sure I understand what the problem with "* proof of * reads *" is, 
> but I hope it helps to know that it comes from the base page.

The problem was syntax, which Ole helped me out with. The error message 
combined with lack of understanding made me focus on inclusion of 
something giving the construct in question an interpretation.

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