def Count.Solution {n m : ℕ} (O : OBdd n m) : Type

Equations

• Count.Solution O = { I : Vector Bool n // O.evaluate I = true }

instance Count.instFintypeSolution {n m : ℕ} {O : OBdd n m} : Fintype (Solution O)

Equations

• Count.instFintypeSolution = Subtype.fintype fun (I : Vector Bool n) => O.evaluate I = true

@[reducible, inline]

abbrev Count.numSolutions {n m : ℕ} (O : OBdd n m) : ℕ

Equations

• Count.numSolutions O = Fintype.card (Count.Solution O)

def Count.count {n m : ℕ} (O : OBdd n m) : ℕ

Equations

• Count.count O = match Count.count_helper✝ O Std.HashMap.emptyWithCapacity ⋯ with | ⟨r, ⋯⟩ => r[(↑O).root]

theorem Count.count_corrent {n m : ℕ} {O : OBdd n m} : count O = numSolutions O