class Repr (α : Type u) : Type u

The standard way of turning values of some type into Format.

When rendered this Format should be as close as possible to something that can be parsed as the input value.

• reprPrec : α → Nat → Std.Format

  Turn a value of type α into a Format at a given precedence. The precedence value can be used to avoid parentheses if they are not necessary.

@[reducible, inline]

abbrev repr {α : Type u_1} [Repr α] (a : α) : Std.Format

Turns a into a Format using its Repr instance. The precedence level is initially set to 0.

@[reducible, inline]

abbrev reprStr {α : Type u_1} [Repr α] (a : α) : String

Turns a into a String using its Repr instance, rendering the Format at the default width of 120 columns.

The precedence level is initially set to 0.

@[reducible, inline]

abbrev reprArg {α : Type u_1} [Repr α] (a : α) : Std.Format

Turns a into a Format using its Repr instance, with the precedence level set to that of function application.

Together with Repr.addAppParen, this can be used to correctly parenthesize function application syntax.

class ReprAtom (α : Type u) : Type

Auxiliary class for marking types that should be considered atomic by Repr methods. We use it at Repr (List α) to decide whether bracketFill should be used or not.

@[implicit_reducible]

instance instReprId {α : Type u_1} [Repr α] : Repr (id α)

@[implicit_reducible]

instance instReprId_1 {α : Type u_1} [Repr α] : Repr (Id α)

@[implicit_reducible]

instance instReprEmpty : Repr Empty

def Bool.repr : Bool → Nat → Std.Format

@[implicit_reducible]

instance instReprBool : Repr Bool

def Repr.addAppParen (f : Std.Format) (prec : Nat) : Std.Format

Adds parentheses to f if the precedence prec from the context is at least that of function application.

Together with reprArg, this can be used to correctly parenthesize function application syntax.

def Decidable.repr {p : Prop} : Decidable p → Nat → Std.Format

@[implicit_reducible]

instance instReprDecidable {p : Prop} : Repr (Decidable p)

@[implicit_reducible]

instance instReprPUnit : Repr PUnit

@[implicit_reducible]

instance instReprULift {α : Type u_1} [Repr α] : Repr (ULift α)

@[implicit_reducible]

instance instReprUnit : Repr Unit

def Option.repr {α : Type u_1} [Repr α] : Option α → Nat → Std.Format

Returns a representation of an optional value that should be able to be parsed as an equivalent optional value.

This function is typically accessed through the Repr (Option α) instance.

@[implicit_reducible]

instance instReprOption {α : Type u_1} [Repr α] : Repr (Option α)

def Sum.repr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] : α ⊕ β → Nat → Std.Format

@[implicit_reducible]

instance instReprSum {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] : Repr (α ⊕ β)

class ReprTuple (α : Type u) : Type u

• reprTuple : α → List Std.Format → List Std.Format

@[implicit_reducible]

instance instReprTupleOfRepr {α : Type u_1} [Repr α] : ReprTuple α

def Prod.reprTuple {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] : α × β → List Std.Format → List Std.Format

@[implicit_reducible]

instance instReprTupleProdOfRepr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] : ReprTuple (α × β)

def Prod.repr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] : α × β → Nat → Std.Format

@[implicit_reducible]

instance instReprProdOfReprTuple {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] : Repr (α × β)

def Sigma.repr {α : Type u_1} {β : α → Type v} [Repr α] [(x : α) → Repr (β x)] : Sigma β → Nat → Std.Format

@[implicit_reducible]

instance instReprSigma {α : Type u_1} {β : α → Type v} [Repr α] [(x : α) → Repr (β x)] : Repr (Sigma β)

@[implicit_reducible]

instance instReprSubtype {α : Type u_1} {p : α → Prop} [Repr α] : Repr (Subtype p)

def Nat.digitChar (n : Nat) : Char

Returns a single digit representation of n, which is assumed to be in a base less than or equal to 16. Returns '*' if n > 15.

Examples:

• Nat.digitChar 5 = '5'
• Nat.digitChar 12 = 'c'
• Nat.digitChar 15 = 'f'
• Nat.digitChar 16 = '*'
• Nat.digitChar 85 = '*'

def Nat.toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char

def Nat.toDigits (base n : Nat) : List Char

Returns the decimal representation of a natural number as a list of digit characters in the given base. If the base is greater than 16 then '*' is returned for digits greater than 0xf.

Examples:

• Nat.toDigits 10 0xff = ['2', '5', '5']
• Nat.toDigits 8 0xc = ['1', '4']
• Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e']
• Nat.toDigits 80 200 = ['2', '*']

@[extern lean_string_of_usize]

def USize.repr (n : USize) : String

Converts a word-sized unsigned integer into a decimal string.

This function is overridden at runtime with an efficient implementation.

Examples:

• USize.repr 0 = "0"
• USize.repr 28 = "28"
• USize.repr 307 = "307"

def Nat.reprFast (n : Nat) : String

@[implemented_by Nat.reprFast]

def Nat.repr (n : Nat) : String

Converts a natural number to its decimal string representation.

def Nat.superDigitChar (n : Nat) : Char

Converts a natural number less than 10 to the corresponding Unicode superscript digit character. Returns '*' for other numbers.

Examples:

• Nat.superDigitChar 3 = '³'
• Nat.superDigitChar 7 = '⁷'
• Nat.superDigitChar 10 = '*'

partial def Nat.toSuperDigitsAux : Nat → List Char → List Char

def Nat.toSuperDigits (n : Nat) : List Char

Converts a natural number to the list of Unicode superscript digit characters that corresponds to its decimal representation.

Examples:

• Nat.toSuperDigits 0 = ['⁰']
• Nat.toSuperDigits 35 = ['³', '⁵']

def Nat.toSuperscriptString (n : Nat) : String

Converts a natural number to a string that contains the its decimal representation as Unicode superscript digit characters.

Examples:

• Nat.toSuperscriptString 0 = "⁰"
• Nat.toSuperscriptString 35 = "³⁵"

def Nat.subDigitChar (n : Nat) : Char

Converts a natural number less than 10 to the corresponding Unicode subscript digit character. Returns '*' for other numbers.

Examples:

• Nat.subDigitChar 3 = '₃'
• Nat.subDigitChar 7 = '₇'
• Nat.subDigitChar 10 = '*'

partial def Nat.toSubDigitsAux : Nat → List Char → List Char

def Nat.toSubDigits (n : Nat) : List Char

Converts a natural number to the list of Unicode subscript digit characters that corresponds to its decimal representation.

Examples:

• Nat.toSubDigits 0 = ['₀']
• Nat.toSubDigits 35 = ['₃', '₅']

def Nat.toSubscriptString (n : Nat) : String

Converts a natural number to a string that contains the its decimal representation as Unicode subscript digit characters.

Examples:

• Nat.toSubscriptString 0 = "₀"
• Nat.toSubscriptString 35 = "₃₅"

@[implicit_reducible]

instance instReprNat : Repr Nat

def Int.repr : Int → String

Returns the decimal string representation of an integer.

@[implicit_reducible]

instance instReprInt : Repr Int

def hexDigitRepr (n : Nat) : String

def Char.quoteCore (c : Char) (inString : Bool := false) : String

def Char.quote (c : Char) : String

Quotes the character to its representation as a character literal, surrounded by single quotes and escaped as necessary.

Examples:

• 'L'.quote = "'L'"
• '"'.quote = "'\\\"'"

@[implicit_reducible]

instance instReprChar : Repr Char

def Char.repr (c : Char) : String

def String.quote (s : String) : String

Converts a string to its corresponding Lean string literal syntax. Double quotes are added to each end, and internal characters are escaped as needed.

Examples:

• "abc".quote = "\"abc\""
• "\"".quote = "\"\\\"\""

@[implicit_reducible]

instance instReprString : Repr String

@[implicit_reducible]

instance instReprRaw : Repr String.Pos.Raw

@[implicit_reducible]

instance instReprRaw_1 : Repr Substring.Raw

@[implicit_reducible]

instance instReprFin (n : Nat) : Repr (Fin n)

@[implicit_reducible]

instance instReprUInt8 : Repr UInt8

@[implicit_reducible]

instance instReprUInt16 : Repr UInt16

@[implicit_reducible]

instance instReprUInt32 : Repr UInt32

@[implicit_reducible]

instance instReprUInt64 : Repr UInt64

@[implicit_reducible]

instance instReprUSize : Repr USize

def List.repr {α : Type u_1} [Repr α] (a : List α) (n : Nat) : Std.Format

@[implicit_reducible]

instance instReprList {α : Type u_1} [Repr α] : Repr (List α)

def List.repr' {α : Type u_1} [Repr α] [ReprAtom α] (a : List α) (n : Nat) : Std.Format

@[implicit_reducible]

instance instReprListOfReprAtom {α : Type u_1} [Repr α] [ReprAtom α] : Repr (List α)

@[implicit_reducible]

instance instReprAtomBool : ReprAtom Bool

@[implicit_reducible]

instance instReprAtomNat : ReprAtom Nat

@[implicit_reducible]

instance instReprAtomInt : ReprAtom Int

@[implicit_reducible]

instance instReprAtomChar : ReprAtom Char

@[implicit_reducible]

instance instReprAtomString : ReprAtom String

@[implicit_reducible]

instance instReprAtomUInt8 : ReprAtom UInt8

@[implicit_reducible]

instance instReprAtomUInt16 : ReprAtom UInt16

@[implicit_reducible]

instance instReprAtomUInt32 : ReprAtom UInt32

@[implicit_reducible]

instance instReprAtomUInt64 : ReprAtom UInt64

@[implicit_reducible]

instance instReprAtomUSize : ReprAtom USize

@[implicit_reducible]

instance instReprSourceInfo : Repr Lean.SourceInfo

def instReprSourceInfo.repr : Lean.SourceInfo → Nat → Std.Format