AlphaGitHub
Source/Packages

Compiler.Planning.Liveness

packages/compiler/planning/src/Compiler/Planning/Liveness.alpha

1,458 lines160 declarations54.8 KiBSHA-256 5734e8062a86
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 257–263

alignmentValid

Full file
257def alignmentValid =
258  (lambda unrestricted alignment : (family ModelWord64) .
259    (nat-eliminate
260      (lambda unrestricted alignmentIsZero : Nat . Nat)
261      (modelWord64IsZero (modelWord64And alignment (modelWord64Subtract alignment modelWord64One)))
262      (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
263      (modelWord64IsZero alignment)))

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.