Documentation

Lean.Data.Format

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