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 → Lean.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 : α) : Lean.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 : α) : Lean.Format

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

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

instance instReprEmpty : Repr Empty

instance instReprBool : Repr Bool

Equations

• instReprBool = { reprPrec := fun (x : Bool) (x_1 : Nat) => match x, x_1 with | true, x => Std.Format.text "true" | false, x => Std.Format.text "false" }

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

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

Equations

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

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 → Lean.Format

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

def Sum.repr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] : α ⊕ β → Nat → Lean.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 (α ⊕ β)

class ReprTuple (α : Type u) : Type u

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

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

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

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

Equations

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

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

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

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

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

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

Equations

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

@[extern lean_string_of_usize]

def USize.repr (n : USize) : String

Equations

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

@[implemented_by _private.Init.Data.Repr.0.Nat.reprFast]

def Nat.repr (n : Nat) : String

Equations

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

def Nat.superDigitChar (n : Nat) : Char

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

Equations

• n.toSuperDigits = n.toSuperDigitsAux []

def Nat.toSuperscriptString (n : Nat) : String

def Nat.subDigitChar (n : Nat) : Char

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

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

Equations

• n.toSubDigits = n.toSubDigitsAux []

def Nat.toSubscriptString (n : Nat) : String

Equations

• n.toSubscriptString = n.toSubDigits.asString

instance instReprNat : Repr Nat

def Int.repr : Int → String

instance instReprInt : Repr Int

def hexDigitRepr (n : Nat) : String

Equations

• hexDigitRepr n = String.singleton n.digitChar

def Char.quoteCore (c : Char) : String

def Char.quoteCore.smallCharToHex (c : Char) : String

def Char.quote (c : Char) : String

instance instReprChar : Repr Char

Equations

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

def Char.repr (c : Char) : String

def String.quote (s : String) : String

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 (s.toString.quote ++ ".toSubstring") }

instance instReprIterator : Repr String.Iterator

Equations

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

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

Equations

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

instance instReprUInt8 : Repr UInt8

instance instReprUInt16 : Repr UInt16

Equations

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

instance instReprUInt32 : Repr UInt32

instance instReprUInt64 : Repr UInt64

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) : Lean.Format

Equations

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

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

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

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

Equations

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

instance instReprAtomBool : ReprAtom Bool

Equations

• instReprAtomBool = { }

instance instReprAtomNat : ReprAtom Nat

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

instance instReprAtomUSize : ReprAtom USize

instance instReprSourceInfo : Repr Lean.SourceInfo