structure Hex.PermGroup.Search.Children {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) {m : Nat} (nodes : Fin m → Node G) (a : Accumulator G P) (k : Nat) (hk : k ≤ m) : Type

The first k children have been visited in order. Earlier certificates are valid against the current accumulator, even after subsequent insertions.

• acc : Accumulator G P
• grows : a.group.IsSubgroup self.acc.group
• certificates : Vector (Certificate C.Reason) k
• checked (i : Fin k) : checkTree C self.acc.group (nodes ⟨↑i, ⋯⟩) self.certificates[↑i] = true

def Hex.PermGroup.Search.Children.collect {n : Nat} {G : Group n} {P : Predicate n} (C : Constraint G P) {m : Nat} (nodes : Fin m → Node G) (visit : (a : Accumulator G P) → (i : Fin m) → Result C (nodes i) a) (a : Accumulator G P) (k : Nat) (hk : k ≤ m) : Children C nodes a k hk

Process children in stored orbit order, carrying the subgroup forward and appending one certificate for every child.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.Children.collect C nodes visit a 0 hk_2 = { acc := a, grows := ⋯, certificates := #v[], checked := ⋯ }