Only consulted after maximum-depth admission has failed. Report the first
begin that would exceed the target's frame bound, in original command order.
860def nativePhysicalRepeatFirstExcess =
861 (lambda unrestricted commands : (family NativePhysicalCommands) .
862 (lambda unrestricted bound : Nat .
863 (app
864 (eliminate
865 NativePhysicalCommands
866 (lambda unrestricted current : (family NativePhysicalCommands) .
867 (pi unrestricted open : Nat . (pi unrestricted ordinal : Nat . Nat)))
868 commands
869 (branch
870 NativePhysicalCommandsEnd
871 .
872 (lambda unrestricted open : Nat . (lambda unrestricted ordinal : Nat . ordinal)))
873 (branch
874 NativePhysicalCommandsNext
875 head
876 tail
877 induction
878 .
879 (lambda unrestricted open : Nat .
880 (lambda unrestricted ordinal : Nat .
881 (eliminate
882 NativePhysicalCommand
883 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
884 head
885 (branch
886 NativePhysicalCommandValue
887 operation
888 identity
889 .
890 (let unrestricted action =
891 (nativePhysicalRepeatAction operation)
892 in
893 (naturalSelect
894 (naturalAnd (naturalEqual action 1) (naturalLessOrEqual bound open))
895 ordinal
896 (induction
897 (naturalSelect
898 (naturalEqual action 1)
899 (succ open)
900 (naturalSaturatingSubtract
901 open
902 (naturalSelect (naturalEqual action 2) 1 0)))
903 (succ ordinal))))))))))
904 0
905 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.