| | Some definitions of interest. |
|
| adjm_size | Def t.size == 1of(t) |
| | | Thm*  t:AdjMatrix. t.size   |
|
| adjmatrix | Def AdjMatrix == size: size  size |
| | | Thm* AdjMatrix Type |
|
| int_seg | Def {i..j } == {k: | i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| 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:| 0i } |
| | | 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 |
