Every edge's frames share the template's storage exactly, and the plan,
frames, state and endpoint state fit the declared arena.
446def nitFramesAdmitted =
447 (lambda unrestricted slots : Nat .
448 (lambda unrestricted system : (family IndependentStateSystem slots) .
449 (lambda unrestricted fanout : Nat .
450 (lambda unrestricted layout : (family NativeIndependentTreeLayout) .
451 (stdListFold
452 Nat
453 Nat
454 (lambda unrestricted index : Nat .
455 (lambda unrestricted rest : Nat .
456 (naturalAnd
457 rest
458 (naturalAnd
459 (naturalEqual
460 (frameEnd (nitCommitmentFor slots system fanout layout (succ index)))
461 (frameEnd (nitCommitment layout)))
462 (naturalEqual
463 (frameEnd (nitReleaseFor slots system fanout layout (succ index)))
464 (frameEnd (nitRelease layout)))))))
465 1
466 (stdListNaturalsBelow (naturalPredecessor (niOwners slots system))))))))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.