- toString : α → String
Instances
- IO.Error.instToStringError
- instToStringByteArray
- instToStringUInt32
- instToStringUInt8
- instToStringSubstring
- instToStringSigma
- instToStringFormat
- EStateM.instToStringResult
- instToStringId
- instToStringDecidable
- instToStringSubtype
- instToStringPUnit
- instToStringUnit
- instToStringOption
- Lean.Syntax.instToStringSyntax
- instToStringUInt64
- instToStringUInt16
- instToStringIterator
- instToStringList
- instToStringSubarray
- instToStringSum
- instToStringFloat
- instToStringNat
- Socket.instToStringSockType
- Socket.instToStringSockAddr
- Socket.instToStringAddressFamily
- Array.instToStringArray
- instToStringProd
- System.instToStringFilePath
- instToStringULift
- instToStringBool
- instToStringFloatArray
- instToStringIdType
- instToStringExcept
- instToStringPos
- Lean.Name.instToStringName
- instToStringString
- instToStringUSize
- instToStringChar
- instToStringFin
- instToStringInt
Equations
- instToStringIdType = inferInstanceAs (ToString α)
Equations
- instToStringId = inferInstanceAs (ToString α)
Equations
- instToStringString = { toString := fun s => s }
Equations
- instToStringSubstring = { toString := fun s => Substring.toString s }
Equations
- instToStringIterator = { toString := fun it => String.Iterator.remainingToString it }
Equations
- instToStringBool = { toString := fun b => cond b "true" "false" }
Equations
- List.toStringAux _fun_discr [] = ""
- List.toStringAux true (x :: xs) = toString x ++ List.toStringAux false xs
- List.toStringAux false (x :: xs) = ", " ++ toString x ++ List.toStringAux false xs
Equations
- List.toString _fun_discr = match _fun_discr with | [] => "[]" | x :: xs => "[" ++ List.toStringAux true (x :: xs) ++ "]"
Equations
- instToStringPUnit = { toString := fun x => "()" }
Equations
- instToStringUnit = { toString := fun x => "()" }
Equations
- instToStringNat = { toString := fun n => Nat.repr n }
Equations
- instToStringPos = { toString := fun p => Nat.repr p.byteIdx }
Equations
- instToStringInt = { toString := fun _fun_discr => match _fun_discr with | Int.ofNat m => toString m | Int.negSucc m => "-" ++ toString (Nat.succ m) }
Equations
- instToStringChar = { toString := fun c => Char.toString c }
Equations
- instToStringFin n = { toString := fun f => toString f.val }
Equations
- instToStringUInt8 = { toString := fun n => toString (UInt8.toNat n) }
Equations
- instToStringUInt16 = { toString := fun n => toString (UInt16.toNat n) }
Equations
- instToStringUInt32 = { toString := fun n => toString (UInt32.toNat n) }
Equations
- instToStringUInt64 = { toString := fun n => toString (UInt64.toNat n) }
Equations
- instToStringUSize = { toString := fun n => toString (USize.toNat n) }
Equations
- instToStringFormat = { toString := fun f => Std.Format.pretty f }
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 ++ ")"
Equations
- String.toInt? s = 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
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
Equations
- String.toInt! s = match String.toInt? s with | some v => v | none => panic "Int expected"
Equations
- instReprExcept = { reprPrec := fun _fun_discr _fun_discr_1 => match _fun_discr, _fun_discr_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 }