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 1331–1349

firstLifetimeError

Full file
1331def firstLifetimeError =
1332  (lambda unrestricted lifetimes : (family Lifetimes) .
1333    (eliminate
1334      Lifetimes
1335      (lambda unrestricted current : (family Lifetimes) . (family LivenessOptionalError))
1336      lifetimes
1337      (branch LifetimesEnd . (constructor LivenessOptionalError LivenessNoError))
1338      (branch
1339        LifetimesNext
1340        head
1341        tail
1342        ih_tail
1343        .
1344        (nat-eliminate
1345          (lambda unrestricted valid : Nat . (family LivenessOptionalError))
1346          (constructor LivenessOptionalError LivenessSomeError (lifetimeError head))
1347          (lambda unrestricted predecessor : Nat .
1348            (lambda unrestricted induction : (family LivenessOptionalError) . ih_tail))
1349          (lifetimeIsValid head)))))

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.