AlphaGitHub
Source/Packages

Compiler.MachineAArch64Assembly

packages/compiler/src/Compiler/MachineAArch64Assembly.alpha

515 lines66 declarations18.9 KiBSHA-256 393650b20792
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 233–242

aarch64DirectionTo

Full file
The direction and byte distance from the referencing word to a target.
233def aarch64DirectionTo =
234  (lambda unrestricted source : Nat .
235    (lambda unrestricted target : Nat .
236      (nat-eliminate
237        (lambda unrestricted backward : Nat . (family AArch64Direction))
238        (constructor AArch64Direction AArch64Forward)
239        (lambda unrestricted predecessor : Nat .
240          (lambda unrestricted induction : (family AArch64Direction) .
241            (constructor AArch64Direction AArch64Backward)))
242        (naturalLess target source))))

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.