543def placementCollision =
544 (lambda unrestricted left : (family Placement) .
545 (lambda unrestricted right : (family Placement) .
546 (eliminate
547 Placement
548 (lambda unrestricted current : (family Placement) . Nat)
549 left
550 (branch
551 PlacementValue
552 leftLifetime
553 leftOffset
554 leftCapacity
555 .
556 (eliminate
557 Placement
558 (lambda unrestricted current : (family Placement) . Nat)
559 right
560 (branch
561 PlacementValue
562 rightLifetime
563 rightOffset
564 rightCapacity
565 .
566 (eliminate
567 Lifetime
568 (lambda unrestricted current : (family Lifetime) . Nat)
569 leftLifetime
570 (branch
571 LifetimeValue
572 leftTensor
573 leftFirst
574 leftLast
575 leftBytes
576 leftAlignment
577 .
578 (eliminate
579 Lifetime
580 (lambda unrestricted current : (family Lifetime) . Nat)
581 rightLifetime
582 (branch
583 LifetimeValue
584 rightTensor
585 rightFirst
586 rightLast
587 rightBytes
588 rightAlignment
589 .
590 (eliminate
591 ModelWord64CheckedResult
592 (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
593 (modelWord64AddChecked
594 (stdByteCountValue leftOffset)
595 (stdByteCountValue leftBytes))
596 (branch
597 ModelWord64CheckedSucceeded
598 leftEnd
599 .
600 (eliminate
601 ModelWord64CheckedResult
602 (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
603 (modelWord64AddChecked
604 (stdByteCountValue rightOffset)
605 (stdByteCountValue rightBytes))
606 (branch
607 ModelWord64CheckedSucceeded
608 rightEnd
609 .
610 (naturalFlagAnd
611 (naturalFlagAnd
612 (naturalLessThanOrEqual
613 (modelWord32ToNatural leftFirst)
614 (modelWord32ToNatural rightLast))
615 (naturalLessThanOrEqual
616 (modelWord32ToNatural rightFirst)
617 (modelWord32ToNatural leftLast)))
618 (naturalFlagAnd
619 (modelWord64LessThan (stdByteCountValue leftOffset) rightEnd)
620 (modelWord64LessThan (stdByteCountValue rightOffset) leftEnd))))
621 (branch ModelWord64CheckedFailed error . (succ zero))))
622 (branch ModelWord64CheckedFailed error . (succ zero)))))))))))))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.