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 244–252

aarch64DistanceTo

Full file
244def aarch64DistanceTo =
245  (lambda unrestricted source : Nat .
246    (lambda unrestricted target : Nat .
247      (nat-eliminate
248        (lambda unrestricted backward : Nat . Nat)
249        (naturalSaturatingSubtract target source)
250        (lambda unrestricted predecessor : Nat .
251          (lambda unrestricted induction : Nat . (naturalSaturatingSubtract source target)))
252        (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.