| | Some definitions of interest. |
|
| ma-compat | Def A ||+ B == A || B & ma-frame-compatible(A; B) & ma-sframe-compatible(A; B) |
|
| Knd | Def Knd == (IdLnk Id)+Id |
| | | Thm* Knd  Type |
|
| IdLnk | Def IdLnk == IdId |
| | | Thm* IdLnk Type |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| 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 |
|
| ma-single-sends | Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; ) |
|
| ma-single-sframe | Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L) |
|
| map | Def map(f;as) == Case of as; nil  nil ; a.as' [(f(a)) / map(f;as')]
Def (recursive) |
| | | Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List |
| | | Thm* A,B:Type, f:(AB), l:A List . map(f;l) B List |
|
| pi1 | Def 1of(t) == t.1 |
| | | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
