Init.Data.Repr

source

class Repr (α : Type u) :

Type u

reprPrec : α → Nat → Lean.Format

Instances

source

@[inline]

abbrev repr {α : Type u_1} [inst : Repr α] (a : α) :

Lean.Format

Equations

repr a = reprPrec a 0

source

@[inline]

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

String

Equations

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

source

@[inline]

abbrev reprArg {α : Type u_1} [inst : Repr α] (a : α) :

Lean.Format

Equations

reprArg a = reprPrec a 1024

source

class ReprAtom (α : Type u) :

Type

Instances

source

instance instReprIdType {α : Type u_1} [inst : Repr α] :

Repr (id α)

Equations

instReprIdType = inferInstanceAs (Repr α)

source

instance instReprId {α : Type u_1} [inst : Repr α] :

Repr (Id α)

Equations

instReprId = inferInstanceAs (Repr α)

source

instance instReprBool:

Repr Bool

Equations

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

source

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

source

instance instReprDecidable {p : Prop} :

Repr (Decidable p)

Equations

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

source

instance instReprPUnit:

Repr PUnit

Equations

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

source

instance instReprULift {α : Type u_1} [inst : Repr α] :

Repr (ULift α)

Equations

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

source

instance instReprUnit:

Repr Unit

Equations

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

source

instance instReprOption {α : Type u_1} [inst : Repr α] :

Repr (Option α)

Equations

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

source

instance instReprSum {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : Repr β] :

Repr (α ⊕ β)

Equations

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

source

class ReprTuple (α : Type u) :

Type u

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

Instances

source

instance instReprTuple {α : Type u_1} [inst : Repr α] :

ReprTuple α

Equations

instReprTuple = { reprTuple := fun a xs => repr a :: xs }

source

instance instReprTupleProd {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : ReprTuple β] :

ReprTuple (α × β)

Equations

instReprTupleProd = { reprTuple := fun x x_1 => match x, x_1 with | (a, b), xs => reprTuple b (repr a :: xs) }

source

instance instReprProd {α : Type u_1} {β : Type u_2} [inst : Repr α] [inst : ReprTuple β] :

Repr (α × β)

Equations

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

source

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

Repr (Sigma β)

Equations

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

source

instance instReprSubtype {α : Type u_1} {p : α → Prop} [inst : Repr α] :

Repr (Subtype p)

Equations

instReprSubtype = { reprPrec := fun s prec => reprPrec s.val prec }

source

def Nat.digitChar (n : Nat) :

Char

Equations

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

source

def Nat.toDigitsCore (base : Nat) :

Nat → Nat → List Char → List Char

Equations

One or more equations did not get rendered due to their size.
Nat.toDigitsCore base 0 _fun_discr _fun_discr = _fun_discr

source

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

List Char

Equations

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

source

def Nat.repr (n : Nat) :

String

Equations

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

source

def Nat.superDigitChar (n : Nat) :

Char

Equations

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

source

partial def Nat.toSuperDigitsAux:

Nat → List Char → List Char

source

def Nat.toSuperDigits (n : Nat) :

List Char

Equations

Nat.toSuperDigits n = Nat.toSuperDigitsAux n []

source

def Nat.toSuperscriptString (n : Nat) :

String

Equations

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

source

instance instReprNat:

Repr Nat

Equations

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

source

def Int.repr:

Int → String

Equations

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

source

instance instReprInt:

Repr Int

Equations

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

source

def hexDigitRepr (n : Nat) :

String

Equations

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

source

def charToHex (c : Char) :

String

Equations

charToHex c = let n := Char.toNat c; let d2 := n / 16; let d1 := n % 16; hexDigitRepr d2 ++ hexDigitRepr d1

source

def Char.quoteCore (c : Char) :

String

Equations

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

source

def Char.quote (c : Char) :

String

Equations

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

source

instance instReprChar:

Repr Char

Equations

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

source

def Char.repr (c : Char) :

String

Equations

Char.repr c = Char.quote c

source

def String.quote (s : String) :

String

Equations

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

source

instance instReprString:

Repr String

Equations

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

source

instance instReprPos:

Repr String.Pos

Equations

instReprPos = { reprPrec := fun p x => Std.Format.text "{ byteIdx := " ++ repr p.byteIdx ++ Std.Format.text " }" }

source

instance instReprSubstring:

Repr Substring

Equations

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

source

instance instReprIterator:

Repr String.Iterator

Equations

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

source

instance instReprFin (n : Nat) :

Repr (Fin n)

Equations

instReprFin n = { reprPrec := fun f x => repr f.val }

source

instance instReprUInt8:

Repr UInt8

Equations

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

source

instance instReprUInt16:

Repr UInt16

Equations

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

source

instance instReprUInt32:

Repr UInt32

Equations

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

source

instance instReprUInt64:

Repr UInt64

Equations

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

source

instance instReprUSize:

Repr USize

Equations

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

source

instance instReprList {α : Type u_1} [inst : Repr α] :

Repr (List α)

Equations

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

source

instance instReprList_1 {α : Type u_1} [inst : Repr α] [inst : ReprAtom α] :

Repr (List α)

Equations

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

source

instance instReprAtomBool:

ReprAtom Bool

Equations

instReprAtomBool = { }

source

instance instReprAtomNat:

ReprAtom Nat

Equations

instReprAtomNat = { }

source

instance instReprAtomInt:

ReprAtom Int

Equations

instReprAtomInt = { }

source

instance instReprAtomChar:

ReprAtom Char

Equations

instReprAtomChar = { }

source

instance instReprAtomString:

ReprAtom String

Equations

instReprAtomString = { }

source

instance instReprAtomUInt8:

ReprAtom UInt8

Equations

instReprAtomUInt8 = { }

source

instance instReprAtomUInt16:

ReprAtom UInt16

Equations

instReprAtomUInt16 = { }

source

instance instReprAtomUInt32:

ReprAtom UInt32

Equations

instReprAtomUInt32 = { }

source

instance instReprAtomUInt64:

ReprAtom UInt64

Equations

instReprAtomUInt64 = { }

source

instance instReprAtomUSize:

ReprAtom USize

Equations

instReprAtomUSize = { }

source

instance instReprSourceInfo:

Repr Lean.SourceInfo

Equations

instReprSourceInfo = { reprPrec := [anonymous] }