c:
. a = b
c
a,b:. (a | b) 
Prop
} == {k:| i 
k < j }m,n:. {m..n} Type}. 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| Some definitions of interest. | |
| divides | c:. a = bc |
| a,b:. (a | b) Prop | |
| int_seg | } == {k:| i k < j } |
| m,n:. {m..n} Type | |
| 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 |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |