| | 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 |
|
| eq_int | Def i= j == if i=j true ; false fi |
| | | Thm* i,j: . (i=j) |
|
| 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 |
|
| l_all | Def (xL.P(x)) == x:T. (x L)  P(x) |
| | | Thm* T:Type, L:T List, P:(TProp). (xL.P(x)) Prop |
|
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | | Thm* A:Type, l:A List. ||l|| |
| | | Thm* ||nil|| |
