pith. machine review for the scientific record. sign in
inductive definition def or abbrev

GateType

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  73inductive GateType
  74  | Input  : GateType   -- leaf node; reads one input variable
  75  | And    : GateType   -- binary conjunction
  76  | Or     : GateType   -- binary disjunction
  77  | Not    : GateType   -- unary negation
  78  | Output : GateType   -- circuit output gate
  79
  80/-- A single gate with its type and parent wire indices.
  81    Wires are numbered 0..(gate_count-1) in topological order,
  82    so parents always have strictly smaller index → DAG guarantee. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.