Init.Data.ToString.Basic

x.toString = match x with | [] => "[]" | [x] => "[" ++ toString x ++ "]" | x :: xs => (List.foldl (fun (x : String) (x_1 : α) => x ++ ", " ++ toString x_1) ("[" ++ toString x) xs).push ']'

source

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

ToString (List α)

Equations

instToStringList = { toString := List.toString }

source

instance instToStringPUnit :

ToString PUnit

Equations

instToStringPUnit = { toString := fun (x : PUnit) => "()" }

source

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

ToString (ULift α)

Equations

instToStringULift = { toString := fun (v : ULift α) => toString v.down }

source

instance instToStringUnit :

ToString Unit

Equations

instToStringUnit = { toString := fun (x : Unit) => "()" }

source

instance instToStringNat :

ToString Nat

Equations

instToStringNat = { toString := fun (n : Nat) => n.repr }

source

instance instToStringPos :

ToString String.Pos

Equations

instToStringPos = { toString := fun (p : String.Pos) => p.byteIdx.repr }

source

instance instToStringInt :

ToString Int

Equations

instToStringInt = { toString := fun (x : Int) => match x with | Int.ofNat m => toString m | Int.negSucc m => "-" ++ toString m.succ }

source

instance instToStringChar :

ToString Char

Equations

instToStringChar = { toString := fun (c : Char) => c.toString }

source

instance instToStringFin (n : Nat) :

ToString (Fin n)

Equations

instToStringFin n = { toString := fun (f : Fin n) => toString ↑f }

source

instance instToStringUInt8 :

ToString UInt8

Equations

instToStringUInt8 = { toString := fun (n : UInt8) => toString n.toNat }

source

instance instToStringUInt16 :

ToString UInt16

Equations

instToStringUInt16 = { toString := fun (n : UInt16) => toString n.toNat }

source

instance instToStringUInt32 :

ToString UInt32

Equations

instToStringUInt32 = { toString := fun (n : UInt32) => toString n.toNat }

source

instance instToStringUInt64 :

ToString UInt64

Equations

instToStringUInt64 = { toString := fun (n : UInt64) => toString n.toNat }

source

instance instToStringUSize :

ToString USize

Equations

instToStringUSize = { toString := fun (n : USize) => toString n.toNat }

source

instance instToStringFormat :

ToString Lean.Format

Equations

instToStringFormat = { toString := fun (f : Lean.Format) => f.pretty Std.Format.defWidth 0 }

source

def addParenHeuristic (s : String) :

String

Equations

addParenHeuristic s = if ("(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s) = true then s else if (!s.any Char.isWhitespace) = true then s else "(" ++ s ++ ")"

source

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

ToString (Option α)

Equations

instToStringOption = { toString := fun (x : Option α) => match x with | none => "none" | some a => "(some " ++ addParenHeuristic (toString a) ++ ")" }

source

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

ToString (α ⊕ β)

Equations

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

source

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

ToString (α × β)

Equations

instToStringProd = { toString := fun (x : α × β) => match x with | (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")" }

source

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

ToString (Sigma β)

Equations

instToStringSigma = { toString := fun (x : Sigma β) => match x with | ⟨a, b⟩ => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩" }

source

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

ToString (Subtype p)

Equations

instToStringSubtype = { toString := fun (s : Subtype p) => toString s.val }

source

def String.toInt? (s : String) :

Option Int

Equations

s.toInt? = if s.get 0 = '-' then do let v ← (s.toSubstring.drop 1).toNat? pure (-Int.ofNat v) else Int.ofNat <$> s.toNat?

source

def String.isInt (s : String) :

Bool

Equations

s.isInt = if s.get 0 = '-' then (s.toSubstring.drop 1).isNat else s.isNat

source

def String.toInt! (s : String) :

Int

Equations

s.toInt! = match s.toInt? with | some v => v | none => panic "Int expected"

source

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

ToString (Except ε α)

Equations

instToStringExcept = { toString := fun (x : Except ε α) => match x with | Except.error e => "error: " ++ toString e | Except.ok a => "ok: " ++ toString a }

source

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

Repr (Except ε α)

Equations

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