Documentation

Init.Data.Nat.Bitwise

theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n 0) :
n / 2 < n
def Nat.bitwise (f : BoolBoolBool) (n : Nat) (m : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[extern lean_nat_land]
    def Nat.land :
    NatNatNat
    Equations
    Instances For
      @[extern lean_nat_lor]
      def Nat.lor :
      NatNatNat
      Equations
      Instances For
        @[extern lean_nat_lxor]
        def Nat.xor :
        NatNatNat
        Equations
        Instances For
          @[extern lean_nat_shiftl]
          def Nat.shiftLeft :
          NatNatNat
          Equations
          Instances For
            @[extern lean_nat_shiftr]
            def Nat.shiftRight :
            NatNatNat
            Equations
            Instances For
              Equations