AlphaGitHub
Source/Packages

Compiler.MachineAArch64

packages/compiler/src/Compiler/MachineAArch64.alpha

1,480 lines362 declarations58.2 KiBSHA-256 16c7a1ba00f1
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 555–567

aarch64ByteWord

Full file
A word from its four little-endian bytes. Every argument is reduced mod 256 by nat-to-byte, so a field that overflows its byte cannot silently corrupt the next one: the smart constructors bound every operand first.
555def aarch64ByteWord =
556  (lambda unrestricted byte0 : Nat .
557    (lambda unrestricted byte1 : Nat .
558      (lambda unrestricted byte2 : Nat .
559        (lambda unrestricted byte3 : Nat .
560          (constructor
561            AArch64EncodeResult
562            AArch64Encoded
563            (bytes-cons
564              (nat-to-byte byte0)
565              (bytes-cons
566                (nat-to-byte byte1)
567                (bytes-cons (nat-to-byte byte2) (bytes-cons (nat-to-byte byte3) b"")))))))))

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.