Zero is balanced; nonzero means an unmatched end or an open frame.
728def nativePhysicalRepeatBalance =
729 (lambda unrestricted commands : (family NativePhysicalCommands) .
730 (app
731 (eliminate
732 NativePhysicalCommands
733 (lambda unrestricted current : (family NativePhysicalCommands) .
734 (pi unrestricted open : Nat . Nat))
735 commands
736 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
737 (branch
738 NativePhysicalCommandsNext
739 head
740 tail
741 induction
742 .
743 (lambda unrestricted open : Nat .
744 (eliminate
745 NativePhysicalCommand
746 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
747 head
748 (branch
749 NativePhysicalCommandValue
750 operation
751 errorIdentity
752 .
753 (eliminate
754 NativePhysicalOperation
755 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
756 operation
757 (branch
758 NativePhysicalSystemCall
759 number
760 arguments
761 payload
762 result
763 .
764 (induction open))
765 (branch
766 NativePhysicalCopyPayloadToState
767 destination
768 extent
769 payload
770 .
771 (induction open))
772 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
773 (branch NativePhysicalFencePoll address expected polls . (induction open))
774 (branch NativePhysicalTelemetryAppend path record . (induction open))
775 (branch NativePhysicalAssertEqual left right error . (induction open))
776 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
777 (branch NativePhysicalHaltSuccess . (induction open))
778 (branch NativePhysicalRepeatBegin count . (induction (succ open)))
779 (branch NativePhysicalSkipUnlessEqual left right count . (induction open))
780 (branch
781 NativePhysicalRepeatEnd
782 .
783 (nat-eliminate
784 (lambda unrestricted count : Nat . Nat)
785 2
786 (lambda unrestricted predecessor : Nat .
787 (lambda unrestricted ignored : Nat . (induction predecessor)))
788 open))
789 (branch
790 NativePhysicalRepeatEndWhen
791 observed
792 expected
793 .
794 (nat-eliminate
795 (lambda unrestricted count : Nat . Nat)
796 2
797 (lambda unrestricted predecessor : Nat .
798 (lambda unrestricted ignored : Nat . (induction predecessor)))
799 open))
800 (branch NativePhysicalStoreWord64 destination value . (induction open))
801 (branch
802 NativePhysicalFenceWait
803 address
804 expected
805 polls
806 interval
807 .
808 (induction open))
809 (branch NativePhysicalRepeatBeginCounted count . (induction (succ open)))
810 (branch NativePhysicalAddWord64 destination left right . (induction open))
811 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
812 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.