Documentation

Init.Data.ToString.Basic

class ToString (α : Type u) :

Type u

toString : α → String

Instances

instance instToStringIdType {α : Type u_1} [inst : ToString α] :

ToString (id α)

Equations

instToStringIdType = inferInstanceAs (ToString α)

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

ToString (Id α)

Equations

instToStringId = inferInstanceAs (ToString α)

instance instToStringString :

ToString String

Equations

instToStringString = { toString := fun s => s }

instance instToStringSubstring :

ToString Substring

Equations

instToStringSubstring = { toString := fun s => Substring.toString s }

instance instToStringIterator :

ToString String.Iterator

Equations

instToStringIterator = { toString := fun it => String.Iterator.remainingToString it }

instance instToStringBool :

Equations

instToStringBool = { toString := fun b => cond b "true" "false" }

instance instToStringDecidable {p : Prop} :

ToString (Decidable p)

Equations

instToStringDecidable = { toString := fun h => match h with | isTrue x => "true" | isFalse x => "false" }

def List.toStringAux {α : Type u} [inst : ToString α] :

Bool → List α → String

Equations

List.toStringAux x [] = ""
List.toStringAux true (x_2 :: xs) = toString x_2 ++ List.toStringAux false xs
List.toStringAux false (x_2 :: xs) = ", " ++ toString x_2 ++ List.toStringAux false xs

def List.toString {α : Type u} [inst : ToString α] :

List α → String

Equations

List.toString x = match x with | [] => "[]" | x :: xs => "[" ++ List.toStringAux true (x :: xs) ++ "]"

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

ToString (List α)

Equations

instToStringList = { toString := List.toString }

instance instToStringPUnit :

Equations

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

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

ToString (ULift α)

Equations

instToStringULift = { toString := fun v => toString v.down }

instance instToStringUnit :

Equations

instToStringUnit = { toString := fun u => "()" }

instance instToStringNat :

Equations

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

instance instToStringInt :

Equations

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

instance instToStringChar :

Equations

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

instance instToStringFin (n : Nat) :

ToString (Fin n)

Equations

instToStringFin n = { toString := fun f => toString f.val }

instance instToStringUInt8 :

Equations

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

instance instToStringUInt16 :

ToString UInt16

Equations

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

instance instToStringUInt32 :

ToString UInt32

Equations

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

instance instToStringUInt64 :

ToString UInt64

Equations

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

instance instToStringUSize :

Equations

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

instance instToStringFormat :

ToString Lean.Format

Equations

instToStringFormat = { toString := fun f => Lean.Format.pretty f }

def addParenHeuristic (s : String) :

Equations

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

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

ToString (Option α)

Equations

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

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

ToString (α ⊕ β)

Equations

instToStringSum = { toString := fun x => match x with | Sum.inl a => "(inl " ++ addParenHeuristic (toString a) ++ ")" | Sum.inr b => "(inr " ++ addParenHeuristic (toString b) ++ ")" }

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

ToString (α × β)

Equations

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

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

ToString (Sigma β)

Equations

instToStringSigma = { toString := fun x => match x with | { fst := a, snd := b } => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩" }

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

ToString (Subtype p)

Equations

instToStringSubtype = { toString := fun s => toString s.val }

def String.toInt? (s : String) :

Equations

String.toInt? s = OptionM.run (if String.get s 0 = Char.ofNat 45 then do let v ← Substring.toNat? (Substring.drop (String.toSubstring s) 1) pure (-Int.ofNat v) else Int.ofNat <$> String.toNat? s)

def String.isInt (s : String) :

Equations

String.isInt s = if String.get s 0 = Char.ofNat 45 then Substring.isNat (Substring.drop (String.toSubstring s) 1) else String.isNat s

def String.toInt! (s : String) :

Equations

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

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

ToString (Except ε α)

Equations

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

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

Repr (Except ε α)

Equations

instReprExcept = { reprPrec := fun x x_1 => match x, x_1 with | Except.error e, prec => Repr.addAppParen (Std.Format.text "Except.error " ++ reprArg e) prec | Except.ok a, prec => Repr.addAppParen (Std.Format.text "Except.ok " ++ reprArg a) prec }