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 124–145

resourceDomainValid

Full file
124def resourceDomainValid =
125  (lambda unrestricted domain : (family ResourceDomain) .
126    (eliminate
127      ResourceDomain
128      (lambda unrestricted current : (family ResourceDomain) . Nat)
129      domain
130      (branch
131        ResourceCapacityDomain
132        id
133        name
134        unit
135        fact
136        .
137        (naturalAnd
138          (naturalLessOrEqual id resourceWordLimit)
139          (naturalAnd (naturalNonzero (bytes-length name)) (resourceFactValid fact))))
140      (branch
141        ResourceRelationDomain
142        id
143        name
144        .
145        (naturalAnd (naturalLessOrEqual id resourceWordLimit) (naturalNonzero (bytes-length name))))))

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.