Wires

References

• Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits

def Circuit.Wires (V : Type u) (I : ℕ) : Type u

Equations

• Circuit.Wires V I = Vector V I

@[implicit_reducible]

instance Circuit.instPreorderWires {V : Type u_1} {I : ℕ} [Preorder V] : Preorder (Wires V I)

Equations

• Circuit.instPreorderWires = { le := fun (a b : Circuit.Wires V I) => ∀ (i : Fin I), Vector.get a i ≤ Vector.get b i, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Circuit.Wires.ext {V : Type u_1} {n : ℕ} {a b : Wires V n} : (∀ (i : Fin n), Vector.get a i = Vector.get b i) → a = b

@[simp]

theorem Circuit.Wires.get_ofFn {n : ℕ} {α : Type u} (f : Fin n → α) (i : Fin n) : (Vector.ofFn f).get i = f i

@[simp]

theorem Circuit.Wires.get_cast {V : Type u_1} {n m : ℕ} (h : n = m) (v : Wires V n) (i : Fin m) : (Vector.cast h v).get i = Vector.get v ⟨↑i, ⋯⟩