814def nativePhysicalRepeatMaximumDepth =
815 (lambda unrestricted commands : (family NativePhysicalCommands) .
816 (app
817 (eliminate
818 NativePhysicalCommands
819 (lambda unrestricted current : (family NativePhysicalCommands) .
820 (pi unrestricted open : Nat . (pi unrestricted highest : Nat . Nat)))
821 commands
822 (branch
823 NativePhysicalCommandsEnd
824 .
825 (lambda unrestricted open : Nat . (lambda unrestricted highest : Nat . highest)))
826 (branch
827 NativePhysicalCommandsNext
828 head
829 tail
830 induction
831 .
832 (lambda unrestricted open : Nat .
833 (lambda unrestricted highest : Nat .
834 (eliminate
835 NativePhysicalCommand
836 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
837 head
838 (branch
839 NativePhysicalCommandValue
840 operation
841 identity
842 .
843 (let unrestricted action =
844 (nativePhysicalRepeatAction operation)
845 in
846 (let unrestricted next =
847 (naturalSelect
848 (naturalEqual action 1)
849 (succ open)
850 (naturalSaturatingSubtract open (naturalSelect (naturalEqual action 2) 1 0)))
851 in
852 (induction
853 next
854 (naturalSelect (naturalLessOrEqual highest next) next highest))))))))))
855 0
856 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.