| | Some definitions of interest. |
|
| 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 |
|
| int_seg | Def {i..j } == {k: | i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| not | Def  A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| search | Def search(k;P) == primrec(k;0; i,j. if 0< j j ; P(i) i+1 else 0 fi) |
| | | Thm* k: , P:(k  ). search(k;P) (k+1) |
|
| primrec | Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| | | Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T |
|
| rev_implies | Def P Q == Q P |
| | | Thm* A,B:Prop. (A B) Prop |
