doc: document some do block patterns/sugar

doc/do.md

@@ -348,6 +348,46 @@ TODO: describe `forIn`
 
 TODO
 
+## Returning early from a failed match
+
+Inside a `do` block, the pattern `let _ ← <success> | <fail>` will continue with the rest of the block if the match on the left hand side succeeds, but will execute the right hand side and exit the block on failure:
+
+```lean
+def showUserInfo (getUsername getFavoriteColor : IO (Option String)) : IO Unit := do
+  let some n ← getUsername | IO.println "no username!"
+  IO.println s!"username: {n}"
+  let some c ← getFavoriteColor | IO.println "user didn't provide a favorite color!"
+  IO.println s!"favorite color: {c}"
+
+-- username: JohnDoe
+-- favorite color: red
+#eval showUserInfo (pure <| some "JohnDoe") (pure <| some "red")
+
+-- no username
+#eval showUserInfo (pure none) (pure <| some "purple")
+
+-- username: JaneDoe
+-- user didn't provide a favorite color
+#eval showUserInfo (pure <| some "JaneDoe") (pure none)
+```
+
+## If-let
+
+Inside a `do` block, users can employ the `if let` pattern to destructure actions:
+
+```lean
+def tryIncrement (getInput : IO (Option Nat)) : IO (Except String Nat) := do
+  if let some n ← getInput
+  then return Except.ok n.succ
+  else return Except.error "argument was `none`"
+
+-- Except.ok 2
+#eval tryIncrement (pure <| some 1)
+
+-- Except.error "argument was `none`"
+#eval tryIncrement (pure <| none)
+```
+
 ## Pattern matching
 
 TODO

doc/expressions.md

@@ -419,33 +419,31 @@ Every computable definition in Lean is compiled to bytecode at definition time.
 
 .. code-block:: lean
 
-    #reduce (λ x, x + 3) 5
-    #eval   (λ x, x + 3) 5
+    #reduce (fun x => x + 3) 5
+    #eval   (fun x => x + 3) 5
 
-    #reduce let x := 5 in x + 3
-    #eval   let x := 5 in x + 3
+    #reduce let x := 5; x + 3
+    #eval   let x := 5; x + 3
 
     def f x := x + 3
 
     #reduce f 5
     #eval   f 5
 
-    #reduce @nat.rec (λ n, Nat) (0 : Nat)
-                     (λ n recval : Nat, recval + n + 1) (5 : Nat)
-    #eval   @nat.rec (λ n, Nat) (0 : Nat)
-                     (λ n recval : Nat, recval + n + 1) (5 : Nat)
+    #reduce @Nat.rec (λ n => Nat) (0 : Nat)
+                     (λ n recval : Nat => recval + n + 1) (5 : Nat)
 
     def g : Nat → Nat
-    | 0     := 0
-    | (n+1) := g n + n + 1
+    | 0     => 0
+    | (n+1) => g n + n + 1
 
     #reduce g 5
     #eval   g 5
 
-    #eval   g 50000
+    #eval   g 5000
 
-    example : (λ x, x + 3) 5 = 8 := rfl
-    example : (λ x, f x) = f := rfl
+    example : (fun x => x + 3) 5 = 8 := rfl
+    example : (fun x => f x) = f := rfl
     example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl
 
 Note: the combination of proof irrelevance and singleton ``Prop`` elimination in ι-reduction renders the ideal version of definitional equality, as described above, undecidable. Lean's procedure for checking definitional equality is only an approximation to the ideal. It is not transitive, as illustrated by the example below. Once again, this does not compromise the consistency or soundness of Lean; it only means that Lean is more conservative in the terms it recognizes as well typed, and this does not cause problems in practice. Singleton elimination will be discussed in greater detail in [Inductive Types](inductive.md).