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 762–779

stdI16ToI8Checked

Full file
762def stdI16ToI8Checked =
763  (lambda unrestricted value : (family StdI16) .
764    (eliminate
765      StdU16
766      (lambda unrestricted current : (family StdU16) . (family StdOption (family StdI8)))
767      (stdI16ToU16 value)
768      (branch
769        StdU16Of
770        low
771        high
772        .
773        (nat-eliminate
774          (lambda unrestricted current : Nat . (family StdOption (family StdI8)))
775          (constructor StdOption StdNone (family StdI8))
776          (lambda unrestricted predecessor : Nat .
777            (lambda unrestricted induction : (family StdOption (family StdI8)) .
778              (constructor StdOption StdSome (family StdI8) (stdI8FromByte low))))
779          (byte-equal high (stdI8SignByte (stdI8FromByte low)))))))

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.