Fixed, explicit trees are admitted without enumerating unrelated fleet
members. Duplicate checking is quadratic in the leaf count; this is not the
future hierarchical fleet planner. A combine runs at one of its child owners,
so every execution role belongs to the declared contribution set.
29def combineContains =
30 (lambda unrestricted role : Nat .
31 (lambda unrestricted members : (family StdList Nat) .
32 (eliminate
33 StdList
34 (lambda unrestricted current : (family StdList Nat) . Nat)
35 members
36 (branch StdListEmpty . 0)
37 (branch StdListCons head tail induction . (naturalOr (naturalEqual role head) 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.