695def validatePlacements =
696 (lambda unrestricted arenaBytes : ByteCount .
697 (lambda unrestricted placements : (family Placements) .
698 (eliminate
699 Placements
700 (lambda unrestricted current : (family Placements) . (family LivenessOptionalError))
701 placements
702 (branch PlacementsEnd . (constructor LivenessOptionalError LivenessNoError))
703 (branch
704 PlacementsNext
705 head
706 tail
707 ih_tail
708 .
709 (nat-eliminate
710 (lambda unrestricted lifetimeInvalid : Nat . (family LivenessOptionalError))
711 (nat-eliminate
712 (lambda unrestricted misaligned : Nat . (family LivenessOptionalError))
713 (nat-eliminate
714 (lambda unrestricted capacityInvalid : Nat . (family LivenessOptionalError))
715 (nat-eliminate
716 (lambda unrestricted rangeInvalid : Nat . (family LivenessOptionalError))
717 ih_tail
718 (lambda unrestricted predecessor : Nat .
719 (lambda unrestricted induction : (family LivenessOptionalError) .
720 (constructor
721 LivenessOptionalError
722 LivenessSomeError
723 (constructor LivenessErrorCode PlacementOutsideArena))))
724 (naturalFlagNot (placementRangeValid arenaBytes head)))
725 (lambda unrestricted predecessor : Nat .
726 (lambda unrestricted induction : (family LivenessOptionalError) .
727 (constructor
728 LivenessOptionalError
729 LivenessSomeError
730 (constructor LivenessErrorCode PlacementCapacityTooSmall))))
731 (naturalFlagNot (placementCapacityValid head)))
732 (lambda unrestricted predecessor : Nat .
733 (lambda unrestricted induction : (family LivenessOptionalError) .
734 (constructor
735 LivenessOptionalError
736 LivenessSomeError
737 (constructor LivenessErrorCode PlacementMisaligned))))
738 (naturalFlagNot (placementAligned head)))
739 (lambda unrestricted predecessor : Nat .
740 (lambda unrestricted induction : (family LivenessOptionalError) .
741 (eliminate
742 Placement
743 (lambda unrestricted current : (family Placement) .
744 (family LivenessOptionalError))
745 head
746 (branch
747 PlacementValue
748 lifetime
749 offset
750 capacity
751 .
752 (constructor LivenessOptionalError LivenessSomeError (lifetimeError lifetime))))))
753 (naturalFlagNot
754 (eliminate
755 Placement
756 (lambda unrestricted current : (family Placement) . Nat)
757 head
758 (branch PlacementValue lifetime offset capacity . (lifetimeIsValid lifetime)))))))))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.