doc: basic documentation

doc/SUMMARY.md

@@ -1,10 +1,12 @@
 # Summary
 
+- [Tour of Lean](./tour.md)
 - [Frequently Asked Questions](./faq.md)
 
 # Language Manual
 
 - [Significant Changes from Lean 3](./lean3changes.md)
+- [String interpolation](./stringinterp.md)
 - [The `do` Notation]()
 
 # Tools

doc/definitions.md

@@ -0,0 +1 @@
+# Definitions

doc/functions.md

@@ -0,0 +1 @@
+# Functions

doc/namespaces.md

@@ -0,0 +1 @@
+# Namespaces

doc/stringinterp.md

@@ -0,0 +1,58 @@
+# 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}"
+```