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.

Equations

• repr a = reprPrec a 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.

Equations

• reprStr a = (reprPrec a 0).pretty

@[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.

Equations

• reprArg a = reprPrec a 1024

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 α)

Equations

• instReprId = inferInstanceAs (Repr α)

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

Equations

• instReprId_1 = inferInstanceAs (Repr α)

instance instReprEmpty : Repr Empty

Equations

• instReprEmpty = { reprPrec := fun (a : Empty) (a_1 : Nat) => nomatch a, a_1 }

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

Equations

• true.repr x✝ = Std.Format.text "true"
• false.repr x✝ = Std.Format.text "false"

instance instReprBool : Repr Bool

Equations

• instReprBool = { reprPrec := Bool.repr }

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.

Equations

• Repr.addAppParen f prec = if prec ≥ 1024 then f.paren else f

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

Equations

• (isTrue h).repr x✝ = Repr.addAppParen (Std.Format.text "isTrue _") x✝
• (isFalse h).repr x✝ = Repr.addAppParen (Std.Format.text "isFalse _") x✝

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

Equations

• instReprDecidable = { reprPrec := Decidable.repr }

instance instReprPUnit : Repr PUnit

Equations

• instReprPUnit = { reprPrec := fun (x : PUnit) (x : Nat) => Std.Format.text "PUnit.unit" }

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

Equations

• instReprULift = { reprPrec := fun (v : ULift α) (prec : Nat) => Repr.addAppParen (Std.Format.text "ULift.up " ++ reprArg v.down) prec }

instance instReprUnit : Repr Unit

Equations

• instReprUnit = { reprPrec := fun (x : Unit) (x : Nat) => Std.Format.text "()" }

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.

Equations

• none.repr x✝ = Std.Format.text "none"
• (some a).repr x✝ = Repr.addAppParen (Std.Format.text "some " ++ reprArg a) x✝

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

Equations

• instReprOption = { reprPrec := Option.repr }

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

Equations

• (Sum.inl a).repr x✝ = Repr.addAppParen (Std.Format.text "Sum.inl " ++ reprArg a) x✝
• (Sum.inr b).repr x✝ = Repr.addAppParen (Std.Format.text "Sum.inr " ++ reprArg b) x✝

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

Equations

• instReprSum = { reprPrec := Sum.repr }

class ReprTuple (α : Type u) : Type u

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

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

Equations

• instReprTupleOfRepr = { reprTuple := fun (a : α) (xs : List Std.Format) => repr a :: xs }

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

Equations

• (a, b).reprTuple x✝ = reprTuple b (repr a :: x✝)

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

Equations

• instReprTupleProdOfRepr = { reprTuple := Prod.reprTuple }

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

Equations

• (a, b).repr x✝ = Std.Format.bracket "(" (Std.Format.joinSep (reprTuple b [repr a]).reverse (Std.Format.text "," ++ Std.Format.line)) ")"

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

Equations

• instReprProdOfReprTuple = { reprPrec := Prod.repr }

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

Equations

• ⟨a, b⟩.repr x✝ = Std.Format.bracket "⟨" (repr a ++ Std.Format.text ", " ++ repr b) "⟩"

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

Equations

• instReprSigma = { reprPrec := Sigma.repr }

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

Equations

• instReprSubtype = { reprPrec := fun (s : Subtype p) (prec : Nat) => reprPrec s.val prec }

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 = '*'

Equations

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

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

Equations

• base.toDigitsCore 0 x✝¹ x✝ = x✝
• base.toDigitsCore fuel.succ x✝¹ x✝ = if x✝¹ / base = 0 then (x✝¹ % base).digitChar :: x✝ else base.toDigitsCore fuel (x✝¹ / base) ((x✝¹ % base).digitChar :: x✝)

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', '*']

Equations

• base.toDigits n = base.toDigitsCore (n + 1) n []

@[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"

Equations

• n.repr = (Nat.toDigits 10 n.toNat).asString

def Nat.reprFast (n : Nat) : String

Equations

• n.reprFast = if h : n < Nat.reprArray✝.size then Nat.reprArray✝¹.getInternal n h else if h : n < USize.size then (USize.ofNatLT n h).repr else (Nat.toDigits 10 n).asString

@[implemented_by Nat.reprFast]

def Nat.repr (n : Nat) : String

Converts a natural number to its decimal string representation.

Equations

• n.repr = (Nat.toDigits 10 n).asString

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 = '*'

Equations

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

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 = ['³', '⁵']

Equations

• n.toSuperDigits = n.toSuperDigitsAux []

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 = "³⁵"

Equations

• n.toSuperscriptString = n.toSuperDigits.asString

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 = '*'

Equations

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

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 = ['₃', '₅']

Equations

• n.toSubDigits = n.toSubDigitsAux []

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 = "₃₅"

Equations

• n.toSubscriptString = n.toSubDigits.asString

instance instReprNat : Repr Nat

Equations

• instReprNat = { reprPrec := fun (n x : Nat) => Std.Format.text n.repr }

def Int.repr : Int → String

Returns the decimal string representation of an integer.

Equations

• (Int.ofNat m).repr = m.repr
• (Int.negSucc m).repr = String.Internal.append "-" m.succ.repr

instance instReprInt : Repr Int

Equations

• instReprInt = { reprPrec := fun (i : Int) (prec : Nat) => if i < 0 then Repr.addAppParen (Std.Format.text i.repr) prec else Std.Format.text i.repr }

def hexDigitRepr (n : Nat) : String

Equations

• hexDigitRepr n = String.singleton n.digitChar

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

Equations

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

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

Equations

• c.quote = String.Internal.append (String.Internal.append "'" c.quoteCore) "'"

instance instReprChar : Repr Char

Equations

• instReprChar = { reprPrec := fun (c : Char) (x : Nat) => Std.Format.text c.quote }

def Char.repr (c : Char) : String

Equations

• c.repr = c.quote

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

Equations

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

instance instReprString : Repr String

Equations

• instReprString = { reprPrec := fun (s : String) (x : Nat) => Std.Format.text s.quote }

instance instReprPos : Repr String.Pos

Equations

• instReprPos = { reprPrec := fun (p : String.Pos) (x : Nat) => Std.Format.text "{ byteIdx := " ++ repr p.byteIdx ++ Std.Format.text " }" }

instance instReprSubstring : Repr Substring

Equations

• instReprSubstring = { reprPrec := fun (s : Substring) (x : Nat) => Std.Format.text (String.Internal.append (Substring.Internal.toString s).quote ".toSubstring") }

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

Equations

• instReprFin n = { reprPrec := fun (f : Fin n) (x : Nat) => repr ↑f }

instance instReprUInt8 : Repr UInt8

Equations

• instReprUInt8 = { reprPrec := fun (n : UInt8) (x : Nat) => repr n.toNat }

instance instReprUInt16 : Repr UInt16

Equations

• instReprUInt16 = { reprPrec := fun (n : UInt16) (x : Nat) => repr n.toNat }

instance instReprUInt32 : Repr UInt32

Equations

• instReprUInt32 = { reprPrec := fun (n : UInt32) (x : Nat) => repr n.toNat }

instance instReprUInt64 : Repr UInt64

Equations

• instReprUInt64 = { reprPrec := fun (n : UInt64) (x : Nat) => repr n.toNat }

instance instReprUSize : Repr USize

Equations

• instReprUSize = { reprPrec := fun (n : USize) (x : Nat) => repr n.toNat }

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

Equations

• [].repr n = Std.Format.text "[]"
• a.repr n = Std.Format.bracket "[" (Std.Format.joinSep a (Std.Format.text "," ++ Std.Format.line)) "]"

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

Equations

• instReprList = { reprPrec := List.repr }

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

Equations

• [].repr' n = Std.Format.text "[]"
• a.repr' n = Std.Format.bracketFill "[" (Std.Format.joinSep a (Std.Format.text "," ++ Std.Format.line)) "]"

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

Equations

• instReprListOfReprAtom = { reprPrec := List.repr' }

instance instReprAtomBool : ReprAtom Bool

Equations

• instReprAtomBool = { }

instance instReprAtomNat : ReprAtom Nat

Equations

• instReprAtomNat = { }

instance instReprAtomInt : ReprAtom Int

Equations

• instReprAtomInt = { }

instance instReprAtomChar : ReprAtom Char

Equations

• instReprAtomChar = { }

instance instReprAtomString : ReprAtom String

Equations

• instReprAtomString = { }

instance instReprAtomUInt8 : ReprAtom UInt8

Equations

• instReprAtomUInt8 = { }

instance instReprAtomUInt16 : ReprAtom UInt16

Equations

• instReprAtomUInt16 = { }

instance instReprAtomUInt32 : ReprAtom UInt32

Equations

• instReprAtomUInt32 = { }

instance instReprAtomUInt64 : ReprAtom UInt64

Equations

• instReprAtomUInt64 = { }

instance instReprAtomUSize : ReprAtom USize

Equations

• instReprAtomUSize = { }

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

Equations

• One or more equations did not get rendered due to their size.
• instReprSourceInfo.repr Lean.SourceInfo.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.SourceInfo.none")).group prec✝

instance instReprSourceInfo : Repr Lean.SourceInfo

Equations

• instReprSourceInfo = { reprPrec := instReprSourceInfo.repr }