i:{k-m..k
}. i+1
m,k:
. k!m 
}. e(i)
Def == if a<
b
f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def (recursive)
f:(A
AA), u:A, a,b:
, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A == {i:| 0
i } TypeB == 
B<Ai,j:. (ij) Prop| Some definitions of interest. | |
| factorial_tail_via_iter | i:{k-m..k}. i+1 |
| m,k:. k!m | |
| iter_via_intseg | }. e(i)
Def == if a< b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def (recursive) |
| f:(AAA), u:A, a,b:, e:({a..b}A). (Iter(f;u) i:{a..b}. e(i)) A | |
| nat | == {i:| 0i } |
| Type | |
| le | B == B<A |
| i,j:. (ij) Prop |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |