IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Guarded Types: T(given P)

Sometimes when describing the intended types of arguments to functions, we want to hedge our typing with some further condition.

For example, the conjunction operator "A & B" of Nuprl is actually what is often called a "cand" or "conditional and", in which the second conjunct is required to be sensible only when the first conjunct is true. Consider the theorem:

Thus, one can naturally express dependent propositions such as "k:. 0<k (2 k)<1", where the truth of the antecedent would entail that the consequent makes sense.

More specifically, the membership of a type "T(given A)" has these properties: for any (closed) expression "e", if "A" is true then eT(given A) just when eT. If "A" is false then eT(given A) unconditionally.