Nuprl - Some Definitions

NOTE: The operator coercing a

to a Prop is normally invisible since it is pretty obvious when it is needed.

assert Def b == if b True else False fi
Thm* b:. b Prop

bor Def p q == if p true else q fi
Thm* p,q:. (p q)

iff Def P Q == (P Q) & (P Q)
Thm* (A B) Prop

bool Def == Unit+Unit
Thm* Type

ifthenelse Def if b t else f fi == dec(b ; t; f)
Thm* b:, A:Type, p,q:A. if b p else q fi A

btrue Def true ==
Thm* true

rev_implies Def P Q == Q P
Thm* (A B) Prop

assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
bor	`Def p q == if p true else q fi` `Thm* p,q:. (p q)`
iff	`Def P Q == (P Q) & (P Q)` `Thm* (A B) Prop`
bool	`Def == Unit+Unit` `Thm* Type`
ifthenelse	`Def if b t else f fi == dec(b ; t; f)` `Thm* b:, A:Type, p,q:A. if b p else q fi A`
btrue	`Def true ==` `Thm* true`
rev_implies	`Def P Q == Q P` `Thm* (A B) Prop`