AlphaGitHub
Source/Packages

Compiler.Planning.Resources

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

636 lines34 declarations25.9 KiBSHA-256 773ccd6b9504
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 89–103

resourceFactValid

Full file
89def resourceFactValid =
90  (lambda unrestricted fact : (family ResourceFact) .
91    (eliminate
92      ResourceFact
93      (lambda unrestricted current : (family ResourceFact) . Nat)
94      fact
95      (branch ResourceAbsent reason . (naturalNonzero (bytes-length reason)))
96      (branch
97        ResourceEstablished
98        limit
99        reference
100        .
101        (naturalAnd
102          (naturalLessOrEqual limit resourceWordLimit)
103          (naturalNonzero (bytes-length reference))))))

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.