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 817–826

aarch64DistanceAccepted

Full file
Forward distances reach modulus/2 - 1 units, backward ones modulus/2.
817def aarch64DistanceAccepted =
818  (lambda unrestricted direction : (family AArch64Direction) .
819    (lambda unrestricted units : Nat .
820      (lambda unrestricted half : Nat .
821        (eliminate
822          AArch64Direction
823          (lambda unrestricted current : (family AArch64Direction) . Nat)
824          direction
825          (branch AArch64Forward . (naturalLess units half))
826          (branch AArch64Backward . (naturalLessOrEqual units half))))))

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.