Documentation

Lean.Data.LBool

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