Nuprl - Some Definitions

Thms finite sets 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

decidable Def Dec(P) == P P
Thm* A:Prop. Dec(A) Prop

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

not Def A == A False
Thm* A:Prop. (A) 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`
decidable	`Def Dec(P) == P P` `Thm* A:Prop. Dec(A) Prop`
iff	`Def P Q == (P Q) & (P Q)` `Thm* A,B:Prop. (A B) Prop`
not	`Def A == A False` `Thm* A:Prop. (A) Prop`
rev_implies	`Def P Q == Q P` `Thm* A,B:Prop. (A B) Prop`