Documentation

Lean.Data.Format

source
def Lean.Std.Format.getWidth (o : Options) :
Nat
Instances For
    source
    def Lean.Std.Format.getIndent (o : Options) :
    Nat
    Instances For
      source
      def Lean.Std.Format.getUnicode (o : Options) :
      Bool
      Instances For
        source
        opaque Lean.Std.Format.format.width :
        Lean.Option Nat
        source
        opaque Lean.Std.Format.format.unicode :
        Lean.Option Bool
        source
        opaque Lean.Std.Format.format.indent :
        Lean.Option Nat
        source
        def Lean.Std.Format.pretty' (f : Format) (o : Options := ∅) :
        String
        Instances For
          source
          @[instance_reducible]
          instance Lean.instToFormatName_lean :
          ToFormat Name
          source
          @[instance_reducible]
          instance Lean.instToFormatDataValue :
          ToFormat DataValue
          source
          @[instance_reducible]
          instance Lean.instToFormatProdNameDataValue :
          ToFormat (Name × DataValue)
          source
          def Lean.formatKVMap (m : KVMap) :
          Format
          Instances For
            source
            @[instance_reducible]
            instance Lean.instToFormatKVMap :
            ToFormat KVMap