Documentation

Lean.Data.LBool

source
inductive Lean.LBool :
Type
Instances For
    source
    def Lean.instInhabitedLBool.default :
    LBool
    Equations
      Instances For
        source
        instance Lean.instInhabitedLBool :
        Inhabited LBool
        Equations
          source
          def Lean.instBEqLBool.beq :
          LBool → LBool → Bool
          Equations
            Instances For
              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