CircuitGate
A gate in a straight-line program representation of a Boolean circuit on n inputs, which can be an input variable indexed by Fin n, a Boolean constant, a NOT gate referencing a previous gate index, or an AND or OR gate referencing two previous gate indices.
Statement
inductive CircuitGate (n : Nat)- Source
- Arora & Barak, Definition 6.2
- Verified
- 10 Sep 2026
- Axioms
- none listed
Read back from the Lean
An inductive type CircuitGate parameterized by a natural number n : Nat, representing a gate in a Boolean circuit with n input variables. It has five constructors:
- var (i : Fin n): represents an input variable indexed by i.
- const (b : Bool): represents a constant Boolean value b.
- not (src : Nat): represents a NOT gate whose input is given by index src.
- and (src1 src2 : Nat): represents an AND gate whose inputs are given by indices src1 and src2.
- or (src1 src2 : Nat): represents an OR gate whose inputs are given by indices src1 and src2.
The type derives DecidableEq and Repr.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- A gate in a straight-line program with n inputs. -/ inductive CircuitGate (n : Nat) where | var (i : Fin n) | const (b : Bool) | not (src : Nat) | and (src1 src2 : Nat) | or (src1 src2 : Nat) deriving DecidableEq, Repr