From 519922eaf43dbb1598d1c73b142a3a42cd6f7269 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Nov 2020 18:42:01 -0800
Subject: [PATCH] doc: basic documentation

---
 doc/SUMMARY.md      |  2 ++
 doc/definitions.md  |  1 +
 doc/functions.md    |  1 +
 doc/namespaces.md   |  1 +
 doc/stringinterp.md | 58 +++++++++++++++++++++++++++++++++++++++++++++
 doc/tour.lean       |  0
 6 files changed, 63 insertions(+)
 create mode 100644 doc/definitions.md
 create mode 100644 doc/functions.md
 create mode 100644 doc/namespaces.md
 create mode 100644 doc/stringinterp.md
 create mode 100644 doc/tour.lean

diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 9fb35bedd6..f66c27ed3a 100644
--- a/doc/SUMMARY.md
+++ b/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
diff --git a/doc/definitions.md b/doc/definitions.md
new file mode 100644
index 0000000000..57e5bd97c4
--- /dev/null
+++ b/doc/definitions.md
@@ -0,0 +1 @@
+# Definitions
diff --git a/doc/functions.md b/doc/functions.md
new file mode 100644
index 0000000000..0c5faf50f8
--- /dev/null
+++ b/doc/functions.md
@@ -0,0 +1 @@
+# Functions
diff --git a/doc/namespaces.md b/doc/namespaces.md
new file mode 100644
index 0000000000..e27fc9e7bf
--- /dev/null
+++ b/doc/namespaces.md
@@ -0,0 +1 @@
+# Namespaces
diff --git a/doc/stringinterp.md b/doc/stringinterp.md
new file mode 100644
index 0000000000..226bf59a9e
--- /dev/null
+++ b/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}"
+```
diff --git a/doc/tour.lean b/doc/tour.lean
new file mode 100644
index 0000000000..e69de29bb2