unsigned order: lexicographic from the high byte down
385def stdU32LessThan =
386 (lambda unrestricted a : (family ModelWord32) .
387 (lambda unrestricted b : (family ModelWord32) .
388 (eliminate
389 ModelWord32
390 (lambda unrestricted current : (family ModelWord32) . Nat)
391 a
392 (branch
393 ModelWord32Value
394 a0
395 a1
396 a2
397 a3
398 .
399 (eliminate
400 ModelWord32
401 (lambda unrestricted current : (family ModelWord32) . Nat)
402 b
403 (branch
404 ModelWord32Value
405 b0
406 b1
407 b2
408 b3
409 .
410 (stdFlagOr
411 (byte-less-than a3 b3)
412 (stdFlagAnd
413 (byte-equal a3 b3)
414 (stdFlagOr
415 (byte-less-than a2 b2)
416 (stdFlagAnd
417 (byte-equal a2 b2)
418 (stdFlagOr
419 (byte-less-than a1 b1)
420 (stdFlagAnd (byte-equal a1 b1) (byte-less-than a0 b0)))))))))))))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.