| Who Cites mklist? |
|
mklist | Def mklist(n;f) == primrec(n;nil; i,l. l @ [(f(i))]) |
| | Thm* T:Type, n: , f:( n T). mklist(n;f) T List |
|
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 |
|
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:( n T T). primrec(n;b;c) T |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |