| | Some definitions of interest. |
|
| list_accum | Def list_accum(x,a.f(x;a);y;l) == Case of l; nil  y ; b.l' list_accum(x,a.f(x;a);f(y;b);l') (recursive) |
| | | Thm*  T,T':Type, l:T List, y:T', f:(T'  TT'). list_accum(x,a.f(x,a);y;l)  T' |
|
| nat | Def  == {i: | 0 i } |
| | | Thm* Type |
|
| primrec | Def primrec(n;b;c) == if n= 0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| | | Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
|
| upto | Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive) |
| | | Thm* i,j:. upto(i;j) {i..j } List |
