a frame's exact value taken into the word's span
678def deviceArenaInclude =
679 (lambda unrestricted ordinal : Nat .
680 (lambda unrestricted offset : Nat .
681 (lambda unrestricted value : Nat .
682 (lambda unrestricted spans : (family DeviceArenaSpans) .
683 (eliminate
684 DeviceArenaSpans
685 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
686 spans
687 (branch
688 DeviceArenaSpansEnd
689 .
690 (constructor
691 DeviceArenaSpans
692 DeviceArenaSpansNext
693 offset
694 (constructor
695 DeviceArenaIntervals
696 DeviceArenaIntervalsNext
697 0
698 0
699 (constructor
700 DeviceArenaIntervals
701 DeviceArenaIntervalsNext
702 value
703 value
704 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)))
705 0
706 0
707 1
708 0
709 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
710 spans))
711 (branch
712 DeviceArenaSpansNext
713 at
714 intervals
715 rise
716 fall
717 uniform
718 last
719 ordinals
720 tail
721 induction
722 .
723 (nat-eliminate
724 (lambda unrestricted same : Nat . (family DeviceArenaSpans))
725 (constructor
726 DeviceArenaSpans
727 DeviceArenaSpansNext
728 at
729 intervals
730 rise
731 fall
732 uniform
733 last
734 ordinals
735 induction)
736 (lambda unrestricted q : Nat .
737 (lambda unrestricted ignored : (family DeviceArenaSpans) .
738 (constructor
739 DeviceArenaSpans
740 DeviceArenaSpansNext
741 at
742 (constructor
743 DeviceArenaIntervals
744 DeviceArenaIntervalsNext
745 value
746 value
747 intervals)
748 rise
749 fall
750 uniform
751 last
752 ordinals
753 tail)))
754 (naturalEqual at offset))))))))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.