def Restrict.orestrict {n m : ℕ} (O : OBdd n m) (b : Bool) (i : Fin n) : OBdd n m

Equations

• Restrict.orestrict O b i = ⟨Restrict.restrict✝ O b i, ⋯⟩

@[simp]

theorem Restrict.orestrict_evaluate {n m : ℕ} {b : Bool} {i : Fin n} {O : OBdd n m} : (orestrict O b i).evaluate = Nary.restrict O.evaluate b i