Part of `shiftCore`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
2050def shiftCorePart1 =
2051 (lambda unrestricted index : Nat .
2052 (lambda unrestricted cutoff : Nat .
2053 (lambda unrestricted amount : Nat .
2054 (nat-eliminate
2055 (lambda unrestricted condition : Nat . (family CoreTerm))
2056 (constructor CoreTerm CoreBound (naturalAdd index amount))
2057 (lambda unrestricted predecessor : Nat .
2058 (lambda unrestricted induction : (family CoreTerm) .
2059 (constructor CoreTerm CoreBound index)))
2060 (nat-less-than index cutoff)))))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.