Init.Data.ToString.Basic

class ToString (α : Type u) :

Types that can be converted into a string for display.

There is no expectation that the resulting string can be parsed back to the original data (see Repr for a similar class with this expectation).

toString : α → String
Converts a value into a string.

Instances

source

@[implicit_reducible]

instance instToStringId {α : Type u_1} [ToString α] :

ToString (id α)

source

@[implicit_reducible]

instance instToStringId_1 {α : Type u_1} [ToString α] :

ToString (Id α)

source

@[implicit_reducible]

instance instToStringString :

ToString String

source

@[implicit_reducible]

instance instToStringRaw :

ToString Substring.Raw

source

@[implicit_reducible]

instance instToStringChar :

ToString Char

source

@[implicit_reducible]

instance instToStringBool :

ToString Bool

source

@[implicit_reducible]

instance instToStringDecidable {p : Prop} :

ToString (Decidable p)

source

@[implicit_reducible]

instance instToStringPUnit :

ToString PUnit

source

@[implicit_reducible]

instance instToStringULift {α : Type u} [ToString α] :

ToString (ULift α)

source

@[implicit_reducible]

instance instToStringUnit :

ToString Unit

source

@[implicit_reducible]

instance instToStringNat :

ToString Nat

source

@[implicit_reducible]

instance instToStringRaw_1 :

ToString String.Pos.Raw

source

@[implicit_reducible]

instance instToStringFin (n : Nat) :

ToString (Fin n)

source

@[implicit_reducible]

instance instToStringUInt8 :

ToString UInt8

source

@[implicit_reducible]

instance instToStringUInt16 :

ToString UInt16

source

@[implicit_reducible]

instance instToStringUInt32 :

ToString UInt32

source

@[implicit_reducible]

instance instToStringUInt64 :

ToString UInt64

source

@[implicit_reducible]

instance instToStringUSize :

ToString USize

source

@[implicit_reducible]

instance instToStringFormat :

ToString Std.Format

source

def addParenHeuristic (s : String) :

String

Instances For

source

@[implicit_reducible]

instance instToStringOption {α : Type u} [ToString α] :

ToString (Option α)

source

@[implicit_reducible]

instance instToStringSum {α : Type u} {β : Type v} [ToString α] [ToString β] :

ToString (α ⊕ β)

source

@[implicit_reducible]

instance instToStringProd {α : Type u} {β : Type v} [ToString α] [ToString β] :

ToString (α × β)

source

@[implicit_reducible]

instance instToStringSigma {α : Type u} {β : α → Type v} [ToString α] [(x : α) → ToString (β x)] :

ToString (Sigma β)

source

@[implicit_reducible]

instance instToStringSubtype {α : Type u} {p : α → Prop} [ToString α] :

ToString (Subtype p)

source

@[implicit_reducible]

instance instToStringExcept {ε : Type u_1} {α : Type u_2} [ToString ε] [ToString α] :

ToString (Except ε α)

source

@[implicit_reducible]

instance instReprExcept {ε : Type u_1} {α : Type u_2} [Repr ε] [Repr α] :

Repr (Except ε α)