58 lines
1.8 KiB
Markdown
58 lines
1.8 KiB
Markdown
# String interpolation
|
|
|
|
The `s!` prefix identifies a string literal as an interpolated string.
|
|
An interpolated string is a string literal that might contain interpolation expressions.
|
|
When an interpolated string is resolved to a result string, items with interpolation expressions are
|
|
replaced by the string representations of the expression results. The polymorphic method `toString` is used
|
|
to convert the value into a string.
|
|
|
|
String interpolation provides a more readable and convenient syntax to create formatted strings than
|
|
a string composite formatting feature. The following example uses both features to produce the same output:
|
|
|
|
```lean
|
|
def name := "John"
|
|
def age := 28
|
|
|
|
#eval IO.println s!"Hello, {name}! Are you {age} years old?"
|
|
|
|
#eval IO.println ("Hello, " ++ name ++ "! Are you " ++ toString age ++ " years old?")
|
|
|
|
-- `println! <interpolated-string>` is a macro for `IO.println s!<interpolated-string>`
|
|
#eval println! "Hello, {name}! Are you {age} years old?"
|
|
```
|
|
|
|
# Structure of an interpolated string
|
|
|
|
To identify a string literal as an interpolated string, prepend it with the `s!`.
|
|
Terms inside braces `{}` are regular expressions whose type implements the type class `ToString`.
|
|
To include a curly brace `{` in your interpolated string, you must escape it using `\{`.
|
|
You nest interpolated strings inside interpolated strings
|
|
|
|
```lean
|
|
def vals := [1, 2, 3]
|
|
|
|
#eval IO.println s!"\{ vals := {vals} }"
|
|
|
|
#eval IO.println s!"variables: {vals.map (fun i => s!"x_{i}")}"
|
|
```
|
|
|
|
# `ToString` instances
|
|
|
|
You can define a `ToString` instance for your own datatypes.
|
|
|
|
```lean
|
|
structure Person :=
|
|
(name : String)
|
|
(age : Nat)
|
|
|
|
instance : ToString Person := {
|
|
toString := fun { name := n, age := v } => s!"\{ name := {n}, age := {v} }"
|
|
}
|
|
|
|
def person1 : Person := {
|
|
name := "John",
|
|
age := 28
|
|
}
|
|
|
|
#eval println! "person1: {person1}"
|
|
```
|