307def nativeCombineFrameIndex =
308 (lambda unrestricted placement : (family NativeCombinePlacement) .
309 (lambda unrestricted identity : (family RegionTransferIdentity) .
310 (app
311 (eliminate
312 StdList
313 (lambda unrestricted current : (family StdList (family RegionTransferIdentity)) .
314 (pi unrestricted index : Nat . Nat))
315 (nativeCombinePayloads (nativeCombinePlacementContext placement))
316 (branch StdListEmpty . (lambda unrestricted index : Nat . index))
317 (branch
318 StdListCons
319 head
320 rest
321 induction
322 .
323 (lambda unrestricted index : Nat .
324 (nat-eliminate
325 (lambda unrestricted flag : Nat . Nat)
326 (induction (naturalAdd index 1))
327 (lambda unrestricted prior : Nat . (lambda unrestricted ignored : Nat . index))
328 (regionTransferIdentityEqual identity head)))))
329 0)))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.