class Repr (α : Type u) : Type u

A typeclass that specifies 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 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

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

@[reducible, inline]

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

@[reducible, inline]

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

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.

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

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

instance instReprEmpty : Repr Empty

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

instance instReprBool : Repr Bool

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

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

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

instance instReprPUnit : Repr PUnit

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

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.

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

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

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

class ReprTuple (α : Type u) : Type u

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

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

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

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

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

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

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"

@[implemented_by _private.Init.Data.Repr.0.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 = "₃₅"

instance instReprNat : Repr Nat

def Int.repr : Int → String

Returns the decimal string representation of an integer.

instance instReprInt : Repr Int

def hexDigitRepr (n : Nat) : String

def Char.quoteCore (c : Char) : String

def Char.quoteCore.smallCharToHex (c : Char) : 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 = "'\\\"'"

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 = "\"\\\"\""

instance instReprString : Repr String

instance instReprPos : Repr String.Pos

instance instReprSubstring : Repr Substring

instance instReprIterator : Repr String.Iterator

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

instance instReprUInt8 : Repr UInt8

instance instReprUInt16 : Repr UInt16

instance instReprUInt32 : Repr UInt32

instance instReprUInt64 : Repr UInt64

instance instReprUSize : Repr USize

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

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

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

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

instance instReprAtomBool : ReprAtom Bool

instance instReprAtomNat : ReprAtom Nat

instance instReprAtomInt : ReprAtom Int

instance instReprAtomChar : ReprAtom Char

instance instReprAtomString : ReprAtom String

instance instReprAtomUInt8 : ReprAtom UInt8

instance instReprAtomUInt16 : ReprAtom UInt16

instance instReprAtomUInt32 : ReprAtom UInt32

instance instReprAtomUInt64 : ReprAtom UInt64

instance instReprAtomUSize : ReprAtom USize

instance instReprSourceInfo : Repr Lean.SourceInfo