| | Some definitions of interest. |
|
| fpf-join | Def f  g == <1of(f) @ filter( a.  a  dom(f);1of(g)),a.f(a)?g(a)> |
|
| append | Def as @ bs == Case of as; nil  bs ; a.as' [a / (as' @ bs)] (recursive) |
| | | Thm*  T:Type, as,bs:T List. (as @ bs) T List |
|
| band | Def p q == if p q else false fi |
| | | Thm* p,q: . (pq) |
|
| fpf | Def a:A fp-> B(a) == d:A List a:{a:A| (a d) }  B(a) |
| | | Thm* A:Type, B:(AType). a:A fp-> B(a) Type |
|
| bnot | Def b == if b false else true fi |
| | | Thm* b:. b |
|
| deq | Def EqDecider(T) == eq:TTx,y:T. x = y    (eq(x,y)) |
| | | Thm* T:Type. EqDecider(T) Type |
|
| deq-member | Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x)  b;false;L) |
|
| fpf-is-empty | Def fpf-is-empty(f) == ||1of(f)||=0 |
|
| 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 |
|
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | | Thm* A:Type, l:A List. ||l|| |
| | | Thm* ||nil|| |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
