class Repr (α : Type u) : Type u

• reprPrec : α → Nat → Lean.Format

@[inline, reducible]

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

@[inline, reducible]

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

@[inline, reducible]

abbrev reprArg {α : Type u_1} [Repr α] (a : α) : Lean.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 instReprIdType {α : Type u_1} [Repr α] : Repr (id α)

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

instance instReprBool : Repr Bool

def Repr.addAppParen (f : Lean.Format) (prec : Nat) : Lean.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 → Lean.Format

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

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

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 instReprTuple {α : Type u_1} [Repr α] : ReprTuple α

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

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

instance instReprProd {α : 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)

def Nat.digitChar (n : Nat) : Char

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

Equations

• Nat.toDigitsCore base 0 x x = x
• Nat.toDigitsCore base (Nat.succ fuel) x x = let d := Nat.digitChar (x % base); let n' := x / base; if n' = 0 then d :: x else Nat.toDigitsCore base fuel n' (d :: x)

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

def Nat.repr (n : Nat) : String

def Nat.superDigitChar (n : Nat) : Char

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

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

def Nat.toSuperscriptString (n : Nat) : String

instance instReprNat : Repr Nat

def Int.repr : Int → String

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

instance instReprChar : Repr Char

def Char.repr (c : Char) : String

def String.quote (s : String) : String

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

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

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

instance instReprList_1 {α : 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