| Who Cites listify? |
|
listify | Def f{m..n} == if nm nil else f(m).f{(m+1)..n} fi (recursive) |
| | Thm* T:Type, m,n:, f:({m..n}T). f{m..n} T List |
|
le_int | Def ij == j<i |
| | Thm* i,j:. (ij) |
|
lt_int | Def i<j == if i<j true ; false fi |
| | Thm* i,j:. (i<j) |
|
bnot | Def b == if b false else true fi |
| | Thm* b:. b |