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 294–315

resourcePlacementValid

Full file
294def resourcePlacementValid =
295  (lambda unrestricted graph : (family ResourceGraph) .
296    (lambda unrestricted placement : (family ResourcePlacement) .
297      (naturalAnd
298        (naturalLessOrEqual (resourcePlacementRole placement) resourceWordLimit)
299        (naturalAnd
300          (naturalNonzero
301            (resourceCount
302              (family ResourceEndpoint)
303              (lambda unrestricted endpoint : (family ResourceEndpoint) .
304                (naturalAnd
305                  (naturalEqual (resourceEndpointId endpoint) (resourcePlacementEndpoint placement))
306                  (naturalAnd
307                    (naturalNonzero
308                      (resourceCount
309                        Bytes
310                        (lambda unrestricted cap : Bytes .
311                          (bytes-equal cap (resourcePlacementCapability placement)))
312                        (resourceEndpointCapabilities endpoint)))
313                    1)))
314              (resourceGraphEndpoints graph)))
315          1))))

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.