1083def nativePhysicalValidateCommands =
1084 (lambda unrestricted commands : (family NativePhysicalCommands) .
1085 (eliminate
1086 NativePhysicalCommands
1087 (lambda unrestricted current : (family NativePhysicalCommands) .
1088 (family NativePhysicalCommandsValidation))
1089 commands
1090 (branch
1091 NativePhysicalCommandsEnd
1092 .
1093 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
1094 (branch
1095 NativePhysicalCommandsNext
1096 head
1097 tail
1098 induction
1099 .
1100 (eliminate
1101 NativePhysicalCommand
1102 (lambda unrestricted current : (family NativePhysicalCommand) .
1103 (family NativePhysicalCommandsValidation))
1104 head
1105 (branch
1106 NativePhysicalCommandValue
1107 operation
1108 errorIdentity
1109 .
1110 (eliminate
1111 NativePhysicalOperationValidation
1112 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1113 (family NativePhysicalCommandsValidation))
1114 (nativePhysicalValidateOperation tail operation)
1115 (branch
1116 NativePhysicalOperationValid
1117 .
1118 (eliminate
1119 NativePhysicalCommandsValidation
1120 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1121 (family NativePhysicalCommandsValidation))
1122 induction
1123 (branch
1124 NativePhysicalCommandsValid
1125 completed
1126 .
1127 (constructor
1128 NativePhysicalCommandsValidation
1129 NativePhysicalCommandsValid
1130 (succ completed)))
1131 (branch
1132 NativePhysicalCommandsInvalid
1133 error
1134 ordinal
1135 .
1136 (constructor
1137 NativePhysicalCommandsValidation
1138 NativePhysicalCommandsInvalid
1139 error
1140 (succ ordinal)))))
1141 (branch
1142 NativePhysicalOperationInvalid
1143 error
1144 .
1145 (constructor
1146 NativePhysicalCommandsValidation
1147 NativePhysicalCommandsInvalid
1148 error
1149 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.