Thm* true Thm* false Thm* b:. b = true b = false
There is a conditional expression whose execution branches on
if X t else r fi if true t else r fi * t if false t else r fi * r
It happens that
A lot of
The Nuprl logic is "constructive" and does not assume that every proposition is either true or false, even when well-defined (see
More acutely, there is no method computationally for branching on the truth or falsity of an arbitrary proposition. So, where one would be inclined to branch on the truth value of a proposition, one instead attempts to formulate the concepts using the type
To mediate between the type of booleans and the type of propositions, we employ a coercion operator,
Def b == if b True else False fi
Trueand Falseare standard true and false propositions.
Normally, except when showing definitions, we suppress the display of the coercion operator itself because it is usually clear whether a boolean or a propositional expression is needed, and it becomes noisy to read. The well-formedness theorem for this coercion is
Here is a sample theorem employing the (invisible) coercion operator to relate
Thm* p,q:. (pq) p & q.
Here are the implicit
p,q:. (pq) p & q.