Nuprl - Some Definitions

Thms choice 1 Sections AutomataTheory Doc

NOTE: This 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

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

refl Def Refl(T;x,y.E(x;y)) == a:T. E(a;a)
Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop

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

About:

assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
iff	`Def P Q == (P Q) & (P Q)` `Thm* A,B:Prop. (A B) Prop`
refl	`Def Refl(T;x,y.E(x;y)) == a:T. E(a;a)` `Thm* T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop`
rev_implies	`Def P Q == Q P` `Thm* A,B:Prop. (A B) Prop`