Equations
Equations
Equations
- instToStringString = { toString := fun (s : String) => s }
Equations
- instToStringIterator = { toString := fun (it : String.Iterator) => it.remainingToString }
Equations
- instToStringBool = { toString := fun (b : Bool) => bif b then "true" else "false" }
Converts a list into a string, using ToString.toString
to convert its elements.
The resulting string resembles list literal syntax, with the elements separated by ", "
and
enclosed in square brackets.
The resulting string may not be valid Lean syntax, because there's no such expectation for
ToString
instances.
Examples:
[1, 2, 3].toString = "[1, 2, 3]"
["cat", "dog"].toString = "[cat, dog]"
["cat", "dog", ""].toString = "[cat, dog, ]"
Equations
Instances For
Equations
- instToStringList = { toString := List.toString }
Equations
- instToStringPUnit = { toString := fun (x : PUnit) => "()" }
Equations
- instToStringUnit = { toString := fun (x : Unit) => "()" }
Equations
- instToStringPos = { toString := fun (p : String.Pos) => p.byteIdx.repr }
Equations
- instToStringFormat = { toString := fun (f : Std.Format) => f.pretty }
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 ++ ")"
Instances For
Interprets a string as the decimal representation of an integer, returning it. Returns none
if
the string does not contain a decimal integer.
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally -
in front. Leading +
characters are not allowed.
Use String.isInt
to check whether String.toInt?
would return some
. String.toInt!
is an
alternative that panics instead of returning none
when the string is not an integer.
Examples:
"".toInt? = none
"-".toInt? = none
"0".toInt? = some 0
"5".toInt? = some 5
"-5".toInt? = some (-5)
"587".toInt? = some 587
"-587".toInt? = some (-587)
" 5".toInt? = none
"2-3".toInt? = none
"0xff".toInt? = none
Equations
Instances For
Checks whether the string can be interpreted as the decimal representation of an integer.
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally -
in front. Leading +
characters are not allowed.
Use String.toInt?
or String.toInt!
to convert such a string to an integer.
Examples:
"".isInt = false
"-".isInt = false
"0".isInt = true
"-0".isInt = true
"5".isInt = true
"587".isInt = true
"-587".isInt = true
"+587".isInt = false
" 5".isInt = false
"2-3".isInt = false
"0xff".isInt = false
Instances For
Interprets a string as the decimal representation of an integer, returning it. Panics if the string does not contain a decimal integer.
A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally -
in front. Leading +
characters are not allowed.
Use String.isInt
to check whether String.toInt!
would return a value. String.toInt?
is a safer
alternative that returns none
instead of panicking when the string is not an integer.
Examples: