Gates

References

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

class Circuit.Gate (V : outParam (Type u_1)) [Preorder V] (G : Type u_2) : Type (max u_1 u_2)

Logic gate.

• inputs : G → ℕ

  The number of input wires of a gate.

• outputs : G → ℕ

  The number of output wires of a gate.

• gate (g : G) : Wires V (inputs g) → Wires V (outputs g)

  The wire-function computed by a gate.

• gate_monotone (g : G) : Monotone (gate g)

  The wire-function of a gate is monotone in the information order.