| | Some definitions of interest. |
|
| deq | Def EqDecider(T) == eq:T  T   x,y:T. x = y    (eq(x,y)) |
| | | Thm* T:Type. EqDecider(T)  Type |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| fpf | Def a:A fp-> B(a) == d:A Lista:{a:A| (a d) }B(a) |
| | | Thm* A:Type, B:(AType). a:A fp-> B(a) Type |
|
| fpf-join | Def f  g == <1of(f) @ filter( a.  a dom(f);1of(g)),a.f(a)?g(a)> |
|
| fpf-dom | Def x dom(f) == deq-member(eq;x;1of(f)) |
|
| iff | Def P Q == (P  Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| so_lambda1 | Def (1. b(1))(1) == b(1) |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
