| | 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 |
|
| l_member | Def (x l) ==  i: . i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| bnot | Def   b == if b false else true fi |
| | | Thm* b:. b |
|
| deq-member | Def deq-member(eq;x;L) == reduce( a,b. eqof(eq)(a,x)  b;false;L) |
|
| filter | Def filter(P;l) == reduce(a,v. if P(a) [a / v] else v fi;nil;l) |
| | | Thm* T:Type, P:(T), l:T List. filter(P;l) T List |
|
| 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 |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
