Unsigned order in four byte comparisons (D17).
424def modelWord32LessThan =
425 (lambda unrestricted left : (family ModelWord32) .
426 (lambda unrestricted right : (family ModelWord32) .
427 (eliminate
428 ModelWord32
429 (lambda unrestricted current : (family ModelWord32) . Nat)
430 left
431 (branch
432 ModelWord32Value
433 l0
434 l1
435 l2
436 l3
437 .
438 (eliminate
439 ModelWord32
440 (lambda unrestricted current : (family ModelWord32) . Nat)
441 right
442 (branch
443 ModelWord32Value
444 r0
445 r1
446 r2
447 r3
448 .
449 (modelWord32OrderByte
450 l3
451 r3
452 (modelWord32OrderByte
453 l2
454 r2
455 (modelWord32OrderByte l1 r1 (modelWord32OrderByte l0 r0 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.