an unrolled loop: body 0 (body 1 (... body (count-1) tail))
158def lsFor =
159 (lambda unrestricted count : Nat .
160 (lambda unrestricted body : (pi unrestricted index : Nat . (pi unrestricted rest : (family SM86Program) . (family SM86Program))) .
161 (lambda unrestricted tail : (family SM86Program) .
162 (nat-eliminate
163 (lambda unrestricted current : Nat . (family SM86Program))
164 tail
165 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family SM86Program) .
166 (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) predecessor) induction)))
167 count))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.