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 258–275

modelWord32FromNaturalTruncated

Full file
258def modelWord32FromNaturalTruncated =
259  (lambda unrestricted value : Nat .
260    (app
261      (nat-eliminate
262        (lambda unrestricted small : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
263        (lambda unrestricted unit : Nat . (modelWord32FromNaturalDivided value))
264        (lambda unrestricted predecessor : Nat .
265          (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
266            (lambda unrestricted unit : Nat .
267              (constructor
268                ModelWord32
269                ModelWord32Value
270                (nat-to-byte value)
271                (byte 0)
272                (byte 0)
273                (byte 0)))))
274        (nat-less-than value byteNaturalTwoHundredFiftySix))
275      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.