Init.Data.Repr

source

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 → Std.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.

Instances

source

@[reducible, inline]

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

Std.Format

Turn a into Format using its Repr instance. The precedence level is initially set to 0.

Equations

repr a = reprPrec a 0

source

@[reducible, inline]

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

String

Equations

reprStr a = (reprPrec a 0).pretty

source

@[reducible, inline]

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

Std.Format

Equations

reprArg a = reprPrec a 1024

source

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.

Instances

source

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

Repr (id α)

Equations

instReprId = inferInstanceAs (Repr α)

source

instance instReprId_1 {α : Type u_1} [Repr α] :

Repr (Id α)

Equations

instReprId_1 = inferInstanceAs (Repr α)

source

instance instReprEmpty :

Repr Empty

Equations

instReprEmpty = { reprPrec := fun (a : Empty) (a_1 : Nat) => nomatch a, a_1 }

source

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" }

source

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

Std.Format

Equations

Repr.addAppParen f prec = if prec ≥ 1024 then f.paren 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 : PUnit) (x : Nat) => Std.Format.text "PUnit.unit" }

source

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 }

source

instance instReprUnit :

Repr Unit

Equations

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

source

def Option.repr {α : Type u_1} [Repr α] :

Option α → Nat → Std.Format

Returns a representation of an optional value that should be able to be parsed as an equivalent optional value.

This function is typically accessed through the Repr (Option α) instance.

Equations

none.repr x✝ = Std.Format.text "none"
(some a).repr x✝ = Repr.addAppParen (Std.Format.text "some " ++ reprArg a) x✝

source

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

Repr (Option α)

Equations

instReprOption = { reprPrec := Option.repr }

source

def Sum.repr {α : Type u_1} {β : Type u_2} [Repr α] [Repr β] :

α ⊕ β → Nat → Std.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✝

source

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

Repr (α ⊕ β)

Equations

instReprSum = { reprPrec := Sum.repr }

source

class ReprTuple (α : Type u) :

Type u

reprTuple : α → List Std.Format → List Std.Format

Instances

source

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

ReprTuple α

Equations

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

source

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

ReprTuple (α × β)

Equations

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

source

def Prod.repr {α : Type u_1} {β : Type u_2} [Repr α] [ReprTuple β] :

α × β → Nat → Std.Format

Equations

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

source

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

Repr (α × β)

Equations

instReprProdOfReprTuple = { reprPrec := Prod.repr }

source

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 => Std.Format.bracket "⟨" (repr a ++ Std.Format.text ", " ++ repr b) "⟩" }

source

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

Repr (Subtype p)

Equations

instReprSubtype = { reprPrec := fun (s : Subtype p) (prec : Nat) => reprPrec s.val prec }

source

def Nat.digitChar (n : Nat) :

Char

Returns a single digit representation of n, which is assumed to be in a base less than or equal to 16. Returns '*' if n > 15.

Examples:

Nat.digitChar 5 = '5'
Nat.digitChar 12 = 'c'
Nat.digitChar 15 = 'f'
Nat.digitChar 16 = '*'
Nat.digitChar 85 = '*'

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

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

source

def Nat.toDigits (base n : Nat) :

List Char

Returns the decimal representation of a natural number as a list of digit characters in the given base. If the base is greater than 16 then '*' is returned for digits greater than 0xf.

Examples:

Nat.toDigits 10 0xff = ['2', '5', '5']
Nat.toDigits 8 0xc = ['1', '4']
Nat.toDigits 16 0xcafe = ['c', 'a', 'f', 'e']
Nat.toDigits 80 200 = ['2', '*']

Equations

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

source

@[extern lean_string_of_usize]

def USize.repr (n : USize) :

String

Converts a word-sized unsigned integer into a decimal string.

This function is overridden at runtime with an efficient implementation.

Examples:

USize.repr 0 = "0"
USize.repr 28 = "28"
USize.repr 307 = "307"

Equations

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

source

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

def Nat.repr (n : Nat) :

String

Converts a natural number to its decimal string representation.

Equations

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

source

def Nat.superDigitChar (n : Nat) :

Char

Converts a natural number less than 10 to the corresponding Unicode superscript digit character. Returns '*' for other numbers.

Examples:

Nat.superDigitChar 3 = '³'
Nat.superDigitChar 7 = '⁷'
Nat.superDigitChar 10 = '*'

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

Converts a natural number to the list of Unicode superscript digit characters that corresponds to its decimal representation.

Examples:

Nat.toSuperDigits 0 = ['⁰']
Nat.toSuperDigits 35 = ['³', '⁵']

Equations

n.toSuperDigits = n.toSuperDigitsAux []

source

def Nat.toSuperscriptString (n : Nat) :

String

Converts a natural number to a string that contains the its decimal representation as Unicode superscript digit characters.

Examples:

Nat.toSuperscriptString 0 = "⁰"
Nat.toSuperscriptString 35 = "³⁵"

Equations

n.toSuperscriptString = n.toSuperDigits.asString

source

def Nat.subDigitChar (n : Nat) :

Char

Converts a natural number less than 10 to the corresponding Unicode subscript digit character. Returns '*' for other numbers.

Examples:

Nat.subDigitChar 3 = '₃'
Nat.subDigitChar 7 = '₇'
Nat.subDigitChar 10 = '*'

Equations

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

source

partial def Nat.toSubDigitsAux :

Nat → List Char → List Char

source

def Nat.toSubDigits (n : Nat) :

List Char

Converts a natural number to the list of Unicode subscript digit characters that corresponds to its decimal representation.

Examples:

Nat.toSubDigits 0 = ['₀']
Nat.toSubDigits 35 = ['₃', '₅']

Equations

n.toSubDigits = n.toSubDigitsAux []

source

def Nat.toSubscriptString (n : Nat) :

String

Converts a natural number to a string that contains the its decimal representation as Unicode subscript digit characters.

Examples:

Nat.toSubscriptString 0 = "₀"
Nat.toSubscriptString 35 = "₃₅"

Equations

n.toSubscriptString = n.toSubDigits.asString

source

instance instReprNat :

Repr Nat

Equations

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

source

def Int.repr :

Int → String

Returns the decimal string representation of an integer.

Equations

(Int.ofNat m).repr = m.repr
(Int.negSucc m).repr = "-" ++ m.succ.repr

source

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 }

source

def hexDigitRepr (n : Nat) :

String

Equations

hexDigitRepr n = String.singleton n.digitChar

source

def Char.quoteCore (c : Char) :

String

Equations

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

source

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

String

Equations

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

source

def Char.quote (c : Char) :

String

Quotes the character to its representation as a character literal, surrounded by single quotes and escaped as necessary.

Examples:

'L'.quote = "'L'"
'"'.quote = "'\\\"'"

Equations

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

source

instance instReprChar :

Repr Char

Equations

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

source

def Char.repr (c : Char) :

String

Equations

c.repr = c.quote

source

def String.quote (s : String) :

String

Converts a string to its corresponding Lean string literal syntax. Double quotes are added to each end, and internal characters are escaped as needed.

Examples: