From 0fc0bf0593b0115ced28393b54db8609031d9d85 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 Nov 2020 18:26:39 -0800
Subject: [PATCH] chore: use `instance ... where` in the docs

---
 doc/lean3changes.md | 5 ++---
 doc/stringinterp.md | 8 ++++----
 doc/tour.md         | 5 ++---
 3 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/doc/lean3changes.md b/doc/lean3changes.md
index c6f68b22f1..522bb37f34 100644
--- a/doc/lean3changes.md
+++ b/doc/lean3changes.md
@@ -47,10 +47,9 @@ here is the example in the link above using Lean 4 implicit lambdas.
 
 ```lean
 # variables (ρ : Type) (m : Type → Type) [Monad m]
-instance : Monad (ReaderT ρ m) := {
-  pure := ReaderT.pure,
+instance : Monad (ReaderT ρ m) where
+  pure := ReaderT.pure
   bind := ReaderT.bind
-}
 ```
 
 Users can disable the implicit lambda feature by using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
diff --git a/doc/stringinterp.md b/doc/stringinterp.md
index 226bf59a9e..8dac400deb 100644
--- a/doc/stringinterp.md
+++ b/doc/stringinterp.md
@@ -45,12 +45,12 @@ structure Person :=
   (name : String)
   (age  : Nat)
 
-instance : ToString Person := {
-  toString := fun { name := n, age := v } => s!"\{ name := {n}, age := {v} }"
-}
+instance : ToString Person where
+  toString : Person -> String
+    | { name := n, age := v } => s!"\{ name := {n}, age := {v} }"
 
 def person1 : Person := {
-  name := "John",
+  name := "John"
   age  := 28
 }
 
diff --git a/doc/tour.md b/doc/tour.md
index d9ee73b6cc..5f185f2a05 100644
--- a/doc/tour.md
+++ b/doc/tour.md
@@ -138,8 +138,8 @@ def isMonday : Weekday → Bool :=
 -- The method `toString` converts values of any type that implements
 -- the class `ToString`.
 -- You can implement instances of `ToString` for your own types.
-instance : ToString Weekday := {
-  toString := fun
+instance : ToString Weekday where
+  toString : Weekday -> String
     | sunday    => "Sunday"
     | monday    => "Monday"
     | tuesday   => "Tuesday"
@@ -147,7 +147,6 @@ instance : ToString Weekday := {
     | thursday  => "Thursday"
     | friday    => "Friday"
     | saturday  => "Saturday"
-}
 
 #eval toString (sunday, 10)