def Printf.errorBadFormat (c : Char) : String

Equations

• Printf.errorBadFormat c = toString "bad formatting char " ++ toString c ++ toString ""

def Printf.errorShortFormat : String

Equations

• Printf.errorShortFormat = "formatting string ended prematurely"

def Printf.errorMissingArgument : String

Equations

• Printf.errorMissingArgument = "argument list ended prematurely"

def Printf.errorBadArgument : String

Equations

• Printf.errorBadArgument = "bad argument"

def Printf.dfmt {f : Type u} [RealFloat f] (c : Char) (p? : Option Int) (alt : Bool) (x : f) : String × String

Equations

• One or more equations did not get rendered due to their size.

inductive Printf.FormatAdjustment : Type

• LeftAdjust : FormatAdjustment
• ZeroPad : FormatAdjustment

instance Printf.instReprFormatAdjustment : Repr FormatAdjustment

Equations

• Printf.instReprFormatAdjustment = { reprPrec := Printf.reprFormatAdjustment✝ }

instance Printf.instInhabitedFormatAdjustment : Inhabited FormatAdjustment

Equations

• Printf.instInhabitedFormatAdjustment = { default := Printf.FormatAdjustment.LeftAdjust }

instance Printf.instDecidableEqFormatAdjustment : DecidableEq FormatAdjustment

Equations

• Printf.instDecidableEqFormatAdjustment x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive Printf.FormatSign : Type

• Plus : FormatSign
• Space : FormatSign

instance Printf.instReprFormatSign : Repr FormatSign

Equations

• Printf.instReprFormatSign = { reprPrec := Printf.reprFormatSign✝ }

instance Printf.instInhabitedFormatSign : Inhabited FormatSign

Equations

• Printf.instInhabitedFormatSign = { default := Printf.FormatSign.Plus }

instance Printf.instDecidableEqFormatSign : DecidableEq FormatSign

Equations

• Printf.instDecidableEqFormatSign x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure Printf.FieldFormat : Type

• width : Option Nat
• precision : Option Int
• adjust : Option FormatAdjustment
• sign : Option FormatSign
• alternate : Bool
• modifiers : String
• char : Char

instance Printf.instReprFieldFormat : Repr FieldFormat

Equations

• Printf.instReprFieldFormat = { reprPrec := Printf.reprFieldFormat✝ }

instance Printf.instInhabitedFieldFormat : Inhabited FieldFormat

Equations

• One or more equations did not get rendered due to their size.

instance Printf.instDecidableEqFieldFormat : DecidableEq FieldFormat

Equations

• Printf.instDecidableEqFieldFormat = Printf.decEqFieldFormat✝

@[reducible, inline]

abbrev Printf.FieldFormatter : Type

Equations

• Printf.FieldFormatter = (Printf.FieldFormat → Printf.ShowS)

structure Printf.FormatParse : Type

Walks over argument-type-specific modifier characters to find primary format character.

• modifiers : String

  Modifiers found

• char : Char

  Primary format character

• rest : String

  Rest of the format string

instance Printf.instReprFormatParse : Repr FormatParse

Equations

• Printf.instReprFormatParse = { reprPrec := Printf.reprFormatParse✝ }

instance Printf.instInhabitedFormatParse : Inhabited FormatParse

Equations

• Printf.instInhabitedFormatParse = { default := { modifiers := default, char := default, rest := default } }

instance Printf.instDecidableEqFormatParse : DecidableEq FormatParse

Equations

• Printf.instDecidableEqFormatParse = Printf.decEqFormatParse✝

@[reducible, inline]

abbrev Printf.ModifierParser : Type

Equations

• Printf.ModifierParser = (String → Printf.FormatParse)

def Printf.intModifierMap : List (String × Int)

Equations

• Printf.intModifierMap = [("hh", Int8.minValue.toInt), ("h", Int16.minValue.toInt), ("l", Int32.minValue.toInt), ("ll", Int64.minValue.toInt), ("L", Int64.minValue.toInt)]

def Printf.parseIntFormat {a : Sort u_1} : a → (s : String) → FormatParse

Equations

• One or more equations did not get rendered due to their size.

def Printf.vFmt (c : Char) (ufmt : FieldFormat) : FieldFormat

Equations

• One or more equations did not get rendered due to their size.
• Printf.vFmt c ufmt = ufmt

def Printf.adjust : FieldFormat → String × String → String

Equations

• One or more equations did not get rendered due to their size.

def Printf.adjustSigned : FieldFormat → String × String → String

Equations

• One or more equations did not get rendered due to their size.
• Printf.adjustSigned x✝¹ x✝ = Printf.adjust x✝¹ x✝

def Printf.integral_prec : Option Int → String → String

Equations

• Printf.integral_prec none x✝ = x✝
• Printf.integral_prec (some 0) "0" = ""
• Printf.integral_prec (some prec) x✝ = "".pushn '0' (prec.toNat - x✝.length) ++ x✝

def Printf.fmti : Option Int → Int → String × String

Equations

• Printf.fmti x✝¹ x✝ = if x✝ < 0 then ("-", Printf.integral_prec x✝¹ (toString "" ++ toString (-x✝) ++ toString "")) else ("", Printf.integral_prec x✝¹ (toString "" ++ toString x✝ ++ toString ""))

def Printf.showIntAtBase {a : Type} [OfNat a 0] [OfNat a 1] [Integral a] [DecidableLT a] [DecidableLE a] [DecidableEq a] : a → (Int → Char) → a → ShowS

Equations

• One or more equations did not get rendered due to their size.

partial def Printf.showIntAtBase.showIt {a : Type} [OfNat a 0] [Integral a] (base : a) (toChr : Int → Char) : a × a → String → String

partial def Printf.fmtu : Int → Option String → Option Int → Option Int → Int → String × String

partial def Printf.fmtu.fmtu' (b : Int) : Option Int → Option Int → Bool → Int → Option String

def Printf.formatString {c : Type u_1} [IsChar c] : List c → FieldFormatter

Equations

• One or more equations did not get rendered due to their size.

def Printf.formatIntegral : Option Int → Int → FieldFormatter

Equations

• One or more equations did not get rendered due to their size.

def Printf.fixupMods (ufmt : FieldFormat) (m : Option Int) : Option Int

Equations

• One or more equations did not get rendered due to their size.

def Printf.formatBoundedInt {a : Type u_1} [Integral a] [Bounded a] : a → FieldFormat → ShowS

Equations

• One or more equations did not get rendered due to their size.

def Printf.formatInt {a : Type u_1} [Integral a] : a → FieldFormat → ShowS

Equations

• Printf.formatInt x✝¹ x✝ = Printf.formatIntegral (Printf.fixupMods x✝ none) (Printf.Integral.toInt x✝¹) x✝

def Printf.formatChar : Char → FieldFormat → ShowS

Equations

• Printf.formatChar x✝¹ x✝ = Printf.formatIntegral (some 0) (Printf.Integral.toInt x✝¹.toNat) (Printf.vFmt 'c' x✝)

def Printf.formatRealFloat {f : Type u} [RealFloat f] : f → FieldFormatter

Equations

• One or more equations did not get rendered due to their size.

class Printf.PrintfArg (a : Type u) : Type u

• formatArg : a → FieldFormatter
• parseFormat : a → ModifierParser

instance Printf.instPrintfArgChar : PrintfArg Char

Equations

• Printf.instPrintfArgChar = { formatArg := Printf.formatChar, parseFormat := fun (x : Char) (cf : String) => Printf.parseIntFormat 0 cf }

instance Printf.instPrintfArgListOfIsChar {c : Type u_1} [IsChar c] : PrintfArg (List c)

Equations

• Printf.instPrintfArgListOfIsChar = { formatArg := Printf.formatString }

instance Printf.instPrintfArgString : PrintfArg String

Equations

• Printf.instPrintfArgString = { formatArg := Printf.formatString ∘ String.toList }

instance Printf.instPrintfArgNat : PrintfArg Nat

Equations

• Printf.instPrintfArgNat = { formatArg := Printf.formatInt, parseFormat := Printf.parseIntFormat }

instance Printf.instPrintfArgInt : PrintfArg Int

Equations

• Printf.instPrintfArgInt = { formatArg := Printf.formatInt, parseFormat := Printf.parseIntFormat }

instance Printf.instPrintfArgOfIntegralOfBounded {a : Type u_1} [Integral a] [Bounded a] : PrintfArg a

Equations

• Printf.instPrintfArgOfIntegralOfBounded = { formatArg := Printf.formatBoundedInt, parseFormat := Printf.parseIntFormat }

instance Printf.instPrintfArgOfRealFloat {a : Type u} [RealFloat a] : PrintfArg a

Equations

• Printf.instPrintfArgOfRealFloat = { formatArg := Printf.formatRealFloat }

@[reducible, inline]

abbrev Printf.UPrintf : Type

Equations

• Printf.UPrintf = (Printf.ModifierParser × Printf.FieldFormatter)

def Printf.getStar : List UPrintf → List UPrintf × Nat

Equations

• One or more equations did not get rendered due to their size.
• Printf.getStar [] = Printf.perror✝ Printf.errorMissingArgument

def Printf.stoi (cs : String) : Int × String

Equations

• Printf.stoi cs = match List.span Char.isDigit cs.toList with | (as, cs') => match as with | [] => (0, cs'.asString) | x => (↑as.asString.toNat!, cs'.asString)

def Printf.adjustment (w p : Option Int) (l z : Bool) : Option FormatAdjustment

Equations

• One or more equations did not get rendered due to their size.

partial def Printf.getSpecs : Bool → Bool → Option FormatSign → Bool → List Char → List UPrintf → FieldFormat × List Char × List UPrintf

partial def Printf.uprintfs : List Char → List UPrintf → ShowS

def Printf.uprintf (format : String) (us : List UPrintf) : String

Equations

• Printf.uprintf format us = Printf.uprintfs format.toList us ""

def Printf.PrintfArg.of {a : Type u_1} [PrintfArg a] (arg : a) : UPrintf

Equations

• Printf.PrintfArg.of arg = (Printf.PrintfArg.parseFormat arg, Printf.PrintfArg.formatArg arg)