AlphaGitHub
Source/Packages

Model.Word32

packages/foundation/standard/src/Model/Word32.alpha

508 lines41 declarations18.3 KiBSHA-256 7f230128ec8c
Download exact fileView at revision426597bda5753d86c4

def · lines 440–471

modelWord32LessThan

Full file
Unsigned order in four byte comparisons (D17).
440def modelWord32LessThan =
441  (lambda unrestricted left : (family ModelWord32) .
442    (lambda unrestricted right : (family ModelWord32) .
443      (eliminate
444        ModelWord32
445        (lambda unrestricted current : (family ModelWord32) . Nat)
446        left
447        (branch
448          ModelWord32Value
449          l0
450          l1
451          l2
452          l3
453          .
454          (eliminate
455            ModelWord32
456            (lambda unrestricted current : (family ModelWord32) . Nat)
457            right
458            (branch
459              ModelWord32Value
460              r0
461              r1
462              r2
463              r3
464              .
465              (modelWord32OrderByte
466                l3
467                r3
468                (modelWord32OrderByte
469                  l2
470                  r2
471                  (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.