chore: use instance ... where in the docs

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.

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
 }
 

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)