1215def nativePhysicalValidateCommands =
1216 (lambda unrestricted commands : (family NativePhysicalCommands) .
1217 (eliminate
1218 NativePhysicalCommands
1219 (lambda unrestricted current : (family NativePhysicalCommands) .
1220 (family NativePhysicalCommandsValidation))
1221 commands
1222 (branch
1223 NativePhysicalCommandsEnd
1224 .
1225 (constructor NativePhysicalCommandsValidation NativePhysicalCommandsValid zero))
1226 (branch
1227 NativePhysicalCommandsNext
1228 head
1229 tail
1230 induction
1231 .
1232 (eliminate
1233 NativePhysicalCommand
1234 (lambda unrestricted current : (family NativePhysicalCommand) .
1235 (family NativePhysicalCommandsValidation))
1236 head
1237 (branch
1238 NativePhysicalCommandValue
1239 operation
1240 errorIdentity
1241 .
1242 (eliminate
1243 NativePhysicalOperationValidation
1244 (lambda unrestricted current : (family NativePhysicalOperationValidation) .
1245 (family NativePhysicalCommandsValidation))
1246 (nativePhysicalValidateOperation tail operation)
1247 (branch
1248 NativePhysicalOperationValid
1249 .
1250 (eliminate
1251 NativePhysicalCommandsValidation
1252 (lambda unrestricted current : (family NativePhysicalCommandsValidation) .
1253 (family NativePhysicalCommandsValidation))
1254 induction
1255 (branch
1256 NativePhysicalCommandsValid
1257 completed
1258 .
1259 (constructor
1260 NativePhysicalCommandsValidation
1261 NativePhysicalCommandsValid
1262 (succ completed)))
1263 (branch
1264 NativePhysicalCommandsInvalid
1265 error
1266 ordinal
1267 .
1268 (constructor
1269 NativePhysicalCommandsValidation
1270 NativePhysicalCommandsInvalid
1271 error
1272 (succ ordinal)))))
1273 (branch
1274 NativePhysicalOperationInvalid
1275 error
1276 .
1277 (constructor
1278 NativePhysicalCommandsValidation
1279 NativePhysicalCommandsInvalid
1280 error
1281 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.