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 40–48

resourceAll

Full file
40def resourceAll =
41  (lambda erased element : Type 0 .
42    (lambda unrestricted predicate : (pi unrestricted value : element . Nat) .
43      (stdListFold
44        element
45        Nat
46        (lambda unrestricted value : element .
47          (lambda unrestricted valid : Nat . (naturalAnd (predicate value) valid)))
48        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.