812def nativePhysicalValidateCommands =
813 (lambda unrestricted commands : (family NativePhysicalCommands) .
814 (eliminate
815 NativePhysicalCommands
816 (lambda unrestricted current : (family NativePhysicalCommands) .
817 (family NativePhysicalCommandsValidation))
818 commands
819 (branch
820 NativePhysicalCommandsEnd
821 .
822 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
823 (branch
824 NativePhysicalCommandsNext
825 head
826 tail
827 induction
828 .
829 (eliminate
830 NativePhysicalCommand
831 (lambda unrestricted current : (family NativePhysicalCommand) .
832 (family NativePhysicalCommandsValidation))
833 head
834 (branch
835 NativePhysicalCommandValue
836 operation
837 errorIdentity
838 .
839 (eliminate
840 NativePhysicalOperationValidation
841 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
842 (family NativePhysicalCommandsValidation))
843 (nativePhysicalValidateOperation operation)
844 (branch
845 NativePhysicalOperationValid
846 .
847 (eliminate
848 NativePhysicalCommandsValidation
849 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
850 (family NativePhysicalCommandsValidation))
851 induction
852 (branch
853 NativePhysicalCommandsValid
854 completed
855 .
856 (constructor
857 NativePhysicalCommandsValidation
858 NativePhysicalCommandsValid
859 (succ completed)))
860 (branch
861 NativePhysicalCommandsInvalid
862 error
863 ordinal
864 .
865 (constructor
866 NativePhysicalCommandsValidation
867 NativePhysicalCommandsInvalid
868 error
869 (succ ordinal)))))
870 (branch
871 NativePhysicalOperationInvalid
872 error
873 .
874 (constructor
875 NativePhysicalCommandsValidation
876 NativePhysicalCommandsInvalid
877 error
878 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.