[Logiweb] No .pdf files & "conditioned definitions"

[Frederik Eriksen]

Hi logiweb at diku.dk,

I have two questions:

#1. When I run the pyk compiler on a certain file with the option 
"level=all", for some reason no .pdf files are generated. Both latex and 
dvipdfm are called, but they return with "result=1". I tried to run pyk 
on a "hello world" file instead, and this gave me no problems. Has 
anyone experienced the same phenomenon?

#2. In math texts you often encounter "conditioned definitions", i.e. 
definitions which only make sense if certain requirements are met. For 
instance, take a look at the following definition:

"Let E be an equivalence relation on a set B, and let b \in B. The 
equivalence class of b modulo E is the set
       (*) [b]_E = {x \in B | xEb}."

(I hope you can read through my quasi-LaTeX notation). The point is that 
the defining equation (*) above only makes sense if 1. E is an 
equivalence relation, 2. b is a member of B.

Is there any way to make such definitions in pyk? I've considered using 
the "endorse" construction, which implements side conditions in proofs, 
but I suspect it's not going to work.

Best Regards
Frederik Eriksen.