Documentation

Lean.Data.LBool

source
inductive Lean.LBool :
Type
Instances For
    source
    instance Lean.instInhabitedLBool :
    Inhabited Lean.LBool
    source
    instance Lean.instBEqLBool :
    BEq Lean.LBool
    source
    def Lean.LBool.neg :
    Lean.LBool → Lean.LBool
    Instances For
      source
      def Lean.LBool.and :
      Lean.LBool → Lean.LBool → Lean.LBool
      Instances For
        source
        def Lean.LBool.toString :
        Lean.LBool → String
        Instances For
          source
          instance Lean.LBool.instToStringLBool :
          ToString Lean.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