Circuits from CSLib

The circuit type and its evaluation are supplied by CSLib. A circuit consists of a shared straight-line program and designated output wires; its size counts only internal gates. Local semantics, costs, and constructions extend this same type.

@[simp]

theorem Algebraic.Circuit.eval_id {σ : Signature} {n : ℕ} {U : Type u} (interpretation : Interpretation σ U) (input : Fin n → U) : (id σ n).eval interpretation input = input

The identity circuit evaluates to its input.