383def modelWord32FromNaturalTruncated =
384 (lambda unrestricted value : Nat .
385 (app
386 (nat-eliminate
387 (lambda unrestricted small : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
388 (lambda unrestricted unit : Nat . (modelWord32FromNaturalDivided value))
389 (lambda unrestricted predecessor : Nat .
390 (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
391 (lambda unrestricted unit : Nat .
392 (constructor
393 ModelWord32
394 ModelWord32Value
395 (nat-to-byte value)
396 (byte 0)
397 (byte 0)
398 (byte 0)))))
399 (nat-less-than value byteNaturalTwoHundredFiftySix))
400 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.