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 379–399

modelWord32ModuloUnchecked

Full file
379def modelWord32ModuloUnchecked =
380  (lambda unrestricted value : (family ModelWord32) .
381    (lambda unrestricted divisor : Nat .
382      (eliminate
383        ModelWord32
384        (lambda unrestricted current : (family ModelWord32) . Nat)
385        value
386        (branch
387          ModelWord32Value
388          b0
389          b1
390          b2
391          b3
392          .
393          (modelWord32ModuloStep
394            (modelWord32ModuloStep
395              (modelWord32ModuloStep (modelWord32ModuloStep zero b3 divisor) b2 divisor)
396              b1
397              divisor)
398            b0
399            divisor)))))

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.