GateType
inductive
The standard Boolean gate types in circuit complexity: conjunction (AND), disjunction (OR), and negation (NOT).
Statement
inductive GateType- Source
- Arora & Barak, Definition 6.1
- Verified
- 10 Sep 2026
- Axioms
- none listed
Read back from the Lean
An inductive type GateType with three nullary constructors: and, or, and not, equipped with derived instances for decidable equality (DecidableEq) and string representation (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
/-- The standard Boolean gate types: AND, OR, and NOT. -/ inductive GateType where | and | or | not deriving DecidableEq, Repr