class Repr (α : Type u) : Type u

• reprPrec : α → Nat → Lean.Format

@[inline, reducible]

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

Equations

• repr a = reprPrec a 0

@[inline, reducible]

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

Equations

• reprStr a = Lean.Format.pretty (reprPrec a 0)

@[inline, reducible]

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

Equations

• instReprIdType = inferInstanceAs (Repr α)

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

Equations

• instReprId = inferInstanceAs (Repr α)

instance instReprBool : Repr Bool

Equations

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

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

Equations

• Repr.addAppParen f prec = if prec ≥ 1024 then Lean.Format.paren f 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

• Option.repr x✝ x = match x✝, x with | none, x => Std.Format.text "none" | some a, prec => Repr.addAppParen (Std.Format.text "some " ++ reprArg a) prec

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

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

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

Equations

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

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

Equations

• instReprTupleProd = { 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

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

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

Equations

• instReprProd = { reprPrec := Prod.repr }

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

Equations

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

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

• 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

Equations

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

def Nat.repr (n : Nat) : String

Equations

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

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

• Nat.toSuperDigits n = Nat.toSuperDigitsAux n []

def Nat.toSuperscriptString (n : Nat) : String

Equations

• Nat.toSuperscriptString n = List.asString (Nat.toSuperDigits n)

instance instReprNat : Repr Nat

Equations

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

def Int.repr : Int → String

Equations

• Int.repr x = match x with | Int.ofNat m => Nat.repr m | Int.negSucc m => "-" ++ Nat.repr (Nat.succ m)

instance instReprInt : Repr Int

Equations

• instReprInt = { reprPrec := fun (i : Int) (x : Nat) => Std.Format.text (Int.repr i) }

def hexDigitRepr (n : Nat) : String

Equations

• hexDigitRepr n = String.singleton (Nat.digitChar n)

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 = let n := Char.toNat c; let d2 := n / 16; let d1 := n % 16; hexDigitRepr d2 ++ hexDigitRepr d1

def Char.quote (c : Char) : String

Equations

• Char.quote c = "'" ++ Char.quoteCore c ++ "'"

instance instReprChar : Repr Char

Equations

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

def Char.repr (c : Char) : String

Equations

• Char.repr c = Char.quote c

def String.quote (s : String) : String

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 (String.quote s) }

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

instance instReprUInt8 : Repr UInt8

Equations

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

instance instReprUInt16 : Repr UInt16

Equations

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

instance instReprUInt32 : Repr UInt32

Equations

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

instance instReprUInt64 : Repr UInt64

Equations

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

instance instReprUSize : Repr USize

Equations

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

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

Equations

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

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

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

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

Equations

• instReprList_1 = { 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✝ }