Circuits

References

• N. D. Belnap, A Useful Four-Valued Logic
• Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits

@[reducible, inline]

abbrev Circuit.and {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

Equations

• Circuit.and = Circuit.CircuitCategory.gate Circuit.BelnapGate.and

@[reducible, inline]

abbrev Circuit.or {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

Equations

• Circuit.or = Circuit.CircuitCategory.gate Circuit.BelnapGate.or

@[reducible, inline]

abbrev Circuit.not {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 1 ⟶ 1

Equations

• Circuit.not = Circuit.CircuitCategory.gate Circuit.BelnapGate.not

@[reducible, inline]

abbrev Circuit.nand {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

Equations

• Circuit.nand = CategoryTheory.CategoryStruct.comp Circuit.and Circuit.not

@[reducible, inline]

abbrev Circuit.nor {C : Type u} [(n : ℕ) → OfNat C n] [CategoryTheory.Category.{u_1, u} C] [CircuitCategory BelnapLevel BelnapGate C] : OfNat.ofNat 2 ⟶ 1

Equations

• Circuit.nor = CategoryTheory.CategoryStruct.comp Circuit.or Circuit.not