Part of `substituteCore`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
2310def substituteCorePart2 =
2311 (lambda unrestricted multiplicity : (family CoreMultiplicity) .
2312 (lambda unrestricted ih_domain : (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm))) .
2313 (lambda unrestricted ih_codomain : (pi unrestricted depth : Nat . (pi unrestricted replacement : (family CoreTerm) . (family CoreTerm))) .
2314 (lambda unrestricted depth : Nat .
2315 (lambda unrestricted replacement : (family CoreTerm) .
2316 (constructor
2317 CoreTerm
2318 CorePi
2319 multiplicity
2320 (ih_domain depth replacement)
2321 (ih_codomain (succ depth) replacement)))))))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.