Documentation

Lean.Data.LBool

source
inductive Lean.LBool :
Type
Instances For
    source
    def Lean.instInhabitedLBool.default :
    LBool
    Instances For
      source
      @[implicit_reducible]
      instance Lean.instInhabitedLBool :
      Inhabited LBool
      source
      def Lean.instBEqLBool.beq :
      LBool → LBool → Bool
      Instances For
        source
        @[implicit_reducible]
        instance Lean.instBEqLBool :
        BEq LBool
        source
        def Lean.LBool.neg :
        LBool → LBool
        Instances For
          source
          def Lean.LBool.and :
          LBool → LBool → LBool
          Instances For
            source
            def Lean.LBool.toString :
            LBool → String
            Instances For
              source
              @[implicit_reducible]
              instance Lean.LBool.instToString :
              ToString LBool
              source
              def Bool.toLBool :
              Bool → Lean.LBool
              Instances For
                source
                @[inline]
                def toLBoolM {m : Type → Type} [Monad m] (x : m Bool) :
                m Lean.LBool
                Instances For