| | Some definitions of interest. |
|
| assert | Def  b == if b True else False fi |
| | | Thm*  b: . b  Prop |
|
| band | Def p  q == if p q else false fi |
| | | Thm* p,q:. (pq) |
|
| 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 |
|
| nat | Def  == {i: | 0 i } |
| | | Thm* Type |
|
| nat_plus | Def  == {i:| 0<i } |
| | | Thm* Type |
|
| sfa_doc_exteq | Def A =ext B == (X:A. X B) & (X:B. X A) |
|
| sfa_doc_sexpr | Def Sexpr(A) == rec(T.(T T)+A) |
| | | Thm* A:Type. Sexpr(A) Type |
|
| top | Def Top == Void(given Void) |
| | | Thm* Top Type |
