Repeats must pair and never nest: 0 means balanced, 1 means a repeat is
still open, 2 means an end without a begin or a begin inside a repeat.
755def nativePhysicalRepeatBalance =
756 (lambda unrestricted commands : (family NativePhysicalCommands) .
757 (app
758 (eliminate
759 NativePhysicalCommands
760 (lambda unrestricted current : (family NativePhysicalCommands) . (pi unrestricted open : Nat . Nat))
761 commands
762 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
763 (branch NativePhysicalCommandsNext head tail induction .
764 (lambda unrestricted open : Nat .
765 (eliminate
766 NativePhysicalCommand
767 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
768 head
769 (branch NativePhysicalCommandValue operation errorIdentity .
770 (eliminate
771 NativePhysicalOperation
772 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
773 operation
774 (branch NativePhysicalSystemCall number arguments payload result . (induction open))
775 (branch NativePhysicalCopyPayloadToState destination extent payload . (induction open))
776 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
777 (branch NativePhysicalFencePoll address expected polls . (induction open))
778 (branch NativePhysicalTelemetryAppend path record . (induction open))
779 (branch NativePhysicalAssertEqual left right error . (induction open))
780 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
781 (branch NativePhysicalHaltSuccess . (induction open))
782 (branch NativePhysicalRepeatBegin count .
783 (nat-eliminate
784 (lambda unrestricted current : Nat . Nat)
785 (induction (succ zero))
786 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2))
787 open))
788 (branch NativePhysicalRepeatEnd .
789 (nat-eliminate
790 (lambda unrestricted current : Nat . Nat)
791 2
792 (lambda unrestricted predecessor : Nat .
793 (lambda unrestricted ignored : Nat .
794 (nat-eliminate
795 (lambda unrestricted current : Nat . Nat)
796 (induction zero)
797 (lambda unrestricted deeper : Nat . (lambda unrestricted ignoredDeeper : Nat . 2))
798 predecessor)))
799 open))
800 (branch NativePhysicalStoreWord64 destination value . (induction open))
801 (branch NativePhysicalFenceWait address expected polls interval . (induction open))
802 (branch NativePhysicalRepeatBeginCounted count .
803 (nat-eliminate
804 (lambda unrestricted current : Nat . Nat)
805 (induction (succ zero))
806 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . 2))
807 open))
808 (branch NativePhysicalAddWord64 destination left right . (induction open))
809 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
810 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.