Documentation

Circuitlib.Circuit.Combinational

Combinational circuits #

References #

source
@[reducible, inline]
abbrev Circuit.CombinationalCircuit :
Type
Equations
Instances For
    source
    @[reducible, inline]
    abbrev Circuit.CombinationalCircuit.and :
    OfNat.ofNat 2 ⟶ 1
    Equations
    Instances For
      source
      @[simp]
      theorem Circuit.CombinationalCircuit.and_def (x y : Bool) :
      ↑and #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && y)]
      source
      @[reducible, inline]
      abbrev Circuit.CombinationalCircuit.or :
      OfNat.ofNat 2 ⟶ 1
      Equations
      Instances For
        source
        @[simp]
        theorem Circuit.CombinationalCircuit.or_def (x y : Bool) :
        ↑or #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x || y)]
        source
        @[reducible, inline]
        abbrev Circuit.CombinationalCircuit.not :
        OfNat.ofNat 1 ⟶ 1
        Equations
        Instances For
          source
          @[simp]
          theorem Circuit.CombinationalCircuit.not_def (x : Bool) :
          ↑not #v[WithBotTop.coe x] = #v[WithBotTop.coe !x]
          source
          @[reducible, inline]
          abbrev Circuit.CombinationalCircuit.nand :
          OfNat.ofNat 2 ⟶ 1
          Equations
          Instances For
            source
            @[simp]
            theorem Circuit.CombinationalCircuit.nand_def (x y : Bool) :
            ↑nand #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe !(x && y)]
            source
            @[reducible, inline]
            abbrev Circuit.CombinationalCircuit.nor :
            OfNat.ofNat 2 ⟶ 1
            Equations
            Instances For
              source
              @[simp]
              theorem Circuit.CombinationalCircuit.nor_def (x y : Bool) :
              ↑nor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe !(x || y)]
              source
              @[reducible, inline]
              abbrev Circuit.CombinationalCircuit.fork :
              OfNat.ofNat 1 ⟶ 2
              Equations
              Instances For
                source
                @[simp]
                theorem Circuit.CombinationalCircuit.fork_def (x : Bool) :
                ↑fork #v[WithBotTop.coe x] = #v[WithBotTop.coe x, WithBotTop.coe x]
                source
                def Circuit.CombinationalCircuit.fork₂ :
                CategoryTheory.MonoidalCategoryStruct.tensorObj (OfNat.ofNat 1) (OfNat.ofNat 1) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj 2 2
                Equations
                Instances For
                  source
                  @[simp]
                  theorem Circuit.CombinationalCircuit.fork₂_def (x y : Bool) :
                  ↑fork₂ #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe x, WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe y]
                  source
                  def Circuit.CombinationalCircuit.copy :
                  OfNat.ofNat 2 ⟶ 4
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem Circuit.CombinationalCircuit.copy_def (x y : Bool) :
                    ↑copy #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe x, WithBotTop.coe y]
                    source
                    def Circuit.CombinationalCircuit.xor :
                    OfNat.ofNat 2 ⟶ 1
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      @[simp]
                      theorem Circuit.CombinationalCircuit.xor_def (x y : Bool) :
                      ↑xor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && !y || !x && y)]
                      source
                      def Circuit.CombinationalCircuit.xnor :
                      OfNat.ofNat 2 ⟶ 1
                      Equations
                      Instances For
                        source
                        @[simp]
                        theorem Circuit.CombinationalCircuit.xnor_def (x y : Bool) :
                        ↑xnor #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && y || !x && !y)]
                        source
                        def Circuit.CombinationalCircuit.halfAdder :
                        OfNat.ofNat 2 ⟶ 2
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[simp]
                          theorem Circuit.CombinationalCircuit.halfAdder_def (x y : Bool) :
                          ↑halfAdder #v[WithBotTop.coe x, WithBotTop.coe y] = #v[WithBotTop.coe (x && !y || !x && y), WithBotTop.coe (x && y)]
                          source
                          def Circuit.CombinationalCircuit.adder :
                          OfNat.ofNat 3 ⟶ 2
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Circuit.CombinationalCircuit.adder_def (x y z : Bool) :
                            ↑adder #v[WithBotTop.coe x, WithBotTop.coe y, WithBotTop.coe z] = #v[WithBotTop.coe ((x && !y || !x && y) && !z || !(x && !y || !x && y) && z), WithBotTop.coe (x && y || (x && !y || !x && y) && z)]