AlphaGitHub
Source/Packages

Compiler.Planning.OrderedCombine

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

832 lines26 declarations41.4 KiBSHA-256 69f52e43e720
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 56–69

combineDistinct

Full file
56def combineDistinct =
57  (lambda unrestricted members : (family StdList Nat) .
58    (eliminate
59      StdList
60      (lambda unrestricted current : (family StdList Nat) . Nat)
61      members
62      (branch StdListEmpty . 1)
63      (branch
64        StdListCons
65        head
66        tail
67        induction
68        .
69        (naturalAnd (naturalIsZero (combineContains 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.