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 883–901

stdU8AddChecked

Full file
883def stdU8AddChecked =
884  (lambda unrestricted a : Byte .
885    (lambda unrestricted b : Byte .
886      (eliminate
887        ByteAddResult
888        (lambda unrestricted current : (family ByteAddResult) . (family StdOption Byte))
889        (byteAddWithCarry a b zero)
890        (branch
891          ByteAddResultValue
892          low
893          carry
894          .
895          (nat-eliminate
896            (lambda unrestricted current : Nat . (family StdOption Byte))
897            (constructor StdOption StdSome Byte low)
898            (lambda unrestricted predecessor : Nat .
899              (lambda unrestricted induction : (family StdOption Byte) .
900                (constructor StdOption StdNone Byte)))
901            carry)))))

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.