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 50–65

resourceDistinct

Full file
50def resourceDistinct =
51  (lambda erased element : Type 0 .
52    (lambda unrestricted same : (pi unrestricted left : element . (pi unrestricted right : element . Nat)) .
53      (lambda unrestricted values : (family StdList element) .
54        (eliminate
55          StdList
56          (lambda unrestricted current : (family StdList element) . Nat)
57          values
58          (branch StdListEmpty . 1)
59          (branch
60            StdListCons
61            head
62            tail
63            induction
64            .
65            (naturalAnd (naturalIsZero (resourceCount element (same head) tail)) induction))))))

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.