Documentation

Lean.Data.LBool

source
inductive Lean.LBool :
Type
Instances For
    source
    @[instance_reducible]
    instance Lean.instInhabitedLBool :
    Inhabited LBool
    source
    @[instance_reducible]
    instance Lean.instBEqLBool :
    BEq LBool
    source
    def Lean.instBEqLBool.beq :
    LBool → LBool → Bool
    Instances For
      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
            @[instance_reducible]
            instance Lean.LBool.instToString :
            ToString LBool
            source
            def Lean.Bool.toLBool :
            Bool → LBool
            Instances For
              source
              @[inline]
              def Lean.toLBoolM {m : Type → Type} [Monad m] (x : m Bool) :
              m LBool
              Instances For