AlphaGitHub
Source/Packages

Std.Word

packages/foundation/standard/src/Std/Word.alpha

1,783 lines192 declarations64.2 KiBSHA-256 27bf8c3f30ee
Download exact fileView at revisionf5034773ad4bb52133

def · lines 685–706

stdU32ToU8Checked

Full file
685def stdU32ToU8Checked =
686  (lambda unrestricted value : (family ModelWord32) .
687    (eliminate
688      ModelWord32
689      (lambda unrestricted current : (family ModelWord32) . (family StdOption Byte))
690      value
691      (branch
692        ModelWord32Value
693        b0
694        b1
695        b2
696        b3
697        .
698        (nat-eliminate
699          (lambda unrestricted current : Nat . (family StdOption Byte))
700          (constructor StdOption StdNone Byte)
701          (lambda unrestricted predecessor : Nat .
702            (lambda unrestricted induction : (family StdOption Byte) .
703              (constructor StdOption StdSome Byte b0)))
704          (stdFlagAnd
705            (byte-equal b1 (byte 0))
706            (stdFlagAnd (byte-equal b2 (byte 0)) (byte-equal b3 (byte 0))))))))

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.