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.

Equations

• repr a = reprPrec a 0

@[reducible, inline]

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

Equations

• reprStr a = (reprPrec a 0).pretty

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

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 }

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

Equations

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

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

Equations

• instReprOption = { reprPrec := Option.repr }

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 (α ⊕ β)

Equations

• instReprSum = { reprPrec := Sum.repr }

class ReprTuple (α : Type u) : Type u

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

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

Equations

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

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

Equations

• instReprTupleProdOfRepr = { reprTuple := fun (x : α × β) (x_1 : List Lean.Format) => match x, x_1 with | (a, b), xs => reprTuple b (repr a :: xs) }

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 (α × β)

Equations

• instReprProdOfReprTuple = { reprPrec := Prod.repr }

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

Equations

• instReprSigma = { reprPrec := fun (x : Sigma β) (x_1 : Nat) => match x, x_1 with | ⟨a, b⟩, x => Lean.Format.bracket "⟨" (repr a ++ Std.Format.text ", " ++ repr b) "⟩" }

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

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 : Nat) (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

Equations

• n.toSuperscriptString = n.toSuperDigits.asString

def Nat.subDigitChar (n : Nat) : Char

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

Equations

• n.toSubDigits = n.toSubDigitsAux []

def Nat.toSubscriptString (n : Nat) : String

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

Equations

• (Int.ofNat m).repr = m.repr
• (Int.negSucc m).repr = "-" ++ 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) : String

Equations

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

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

Equations

• Char.quoteCore.smallCharToHex c = hexDigitRepr (c.toNat / 16) ++ hexDigitRepr (c.toNat % 16)

def Char.quote (c : Char) : String

Equations

• c.quote = "'" ++ 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

Equations

• s.quote = if s.isEmpty = true then "\"\"" else String.foldl (fun (s : String) (c : Char) => s ++ c.quoteCore) "\"" s ++ "\""

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

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

Equations

• instReprList = { reprPrec := List.repr }

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

Equations

• [].repr' n = Std.Format.text "[]"
• a.repr' n = Std.Format.bracketFill "[" (Lean.Format.joinSep a (Std.Format.text "," ++ Lean.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 = { }

instance instReprSourceInfo : Repr Lean.SourceInfo

Equations

• instReprSourceInfo = { reprPrec := reprSourceInfo✝ }