Erase errors in code examples in lean\main.

lean/main/01_intro.lean

@@ -128,8 +128,13 @@ elab "#assertType " termStx:term " : " typeStx:term : command =>
       logInfo "success"
     catch | _ => throwError "failure"
 
-#assertType 5  : Nat -- success
-#assertType [] : Nat -- failure
+/-- info: success -/
+#guard_msgs in --#
+#assertType 5  : Nat
+
+/-- error: failure -/
+#guard_msgs in --#
+#assertType [] : Nat
 
 /-! We started by using `elab` to define a `command` syntax. When parsed
 by the compiler, it will trigger the incoming computation.

lean/main/05_syntax.lean

@@ -154,7 +154,7 @@ We can now write `MyTerm` in place of things like `1 + 1` and it will be
 it just means that the Lean parser can understand it:
 -/
 
-def Playground1.test := MyTerm
+#check_failure MyTerm
 -- elaboration function for 'termMyTerm' has not been implemented
 --   MyTerm
 
@@ -182,7 +182,7 @@ scoped syntax "⊥" : term -- ⊥ for false
 scoped syntax "⊤" : term -- ⊤ for true
 scoped syntax:40 term " OR " term : term
 scoped syntax:50 term " AND " term : term
-#check ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
+#check_failure ⊥ OR (⊤ AND ⊥) -- elaboration function hasn't been implemented but parsing passes
 
 end Playground2
 
@@ -203,9 +203,11 @@ syntax:50 boolean_expr " AND " boolean_expr : boolean_expr
 Now that we are working in our own syntax category, we are completely
 disconnected from the rest of the system. And these cannot be used in place of
 terms anymore:
--/
 
+```lean
 #check ⊥ AND ⊤ -- expected term
+```
+-/
 
 /-!
 In order to integrate our syntax category into the rest of the system we will
@@ -214,7 +216,7 @@ will re-embed it into the `term` category:
 -/
 
 syntax "[Bool|" boolean_expr "]" : term
-#check [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
+#check_failure [Bool| ⊥ AND ⊤] -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ### Syntax combinators
@@ -272,23 +274,25 @@ syntax binNumber := binDigit,+
 /-!
 Since we can just use named parsers in place of syntax categories, we can now easily
 add this to the `term` category:
--/
 
+```lean
 syntax "bin(" binNumber ")" : term
 #check bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 #check bin() -- fails to parse because `binNumber` is "one or many": expected 'O' or 'Z'
+```
+-/
 
 syntax binNumber' := binDigit,* -- note the *
 syntax "emptyBin(" binNumber' ")" : term
-#check emptyBin() -- elaboration function hasn't been implemented but parsing passes
+#check_failure emptyBin() -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 Note that nothing is limiting us to only using one syntax combinator per parser,
 we could also have written all of this inline:
 -/
 
 syntax "binCompact(" ("Z" <|> "O"),+ ")" : term
-#check binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binCompact(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 As a final feature, let's add an optional string comment that explains the binary
@@ -297,8 +301,8 @@ literal being declared:
 
 -- The (...)? syntax means that the part in parentheses is optional
 syntax "binDoc(" (str ";")? binNumber ")" : term
-#check binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
-#check binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+#check_failure binDoc("mycomment"; Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
 
 /-!
 ## Operating on Syntax

lean/main/06_macros.lean

@@ -410,8 +410,8 @@ macro_rules
   -- in this case `error_position`, giving it the name `tk`
   | `(error_position%$tk first) => withRef tk (Macro.throwError "Ahhh")
 
-#eval error_position all -- the error is indicated at `error_position all`
-#eval error_position first -- the error is only indicated at `error_position`
+#check_failure error_position all -- the error is indicated at `error_position all`
+#check_failure error_position first -- the error is only indicated at `error_position`
 
 /-
 Obviously controlling the positions of errors in this way is quite important

lean/main/07_elaboration.lean

@@ -260,7 +260,7 @@ this information to complete elaboration.
 We can also easily provoke cases where this does not work out. For example:
 -/
 
-#check set_option trace.Elab.postpone true in List.foldr .add
+#check_failure set_option trace.Elab.postpone true in List.foldr .add
 -- [Elab.postpone] .add : ?m.5808 → ?m.5809 → ?m.5809
 -- invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
   -- ?m.5808 → ?m.5809 → ?m.5809
@@ -328,9 +328,9 @@ def myanonImpl : TermElab := fun stx typ? => do
   elabTerm stx typ -- call term elaboration recursively
 
 #check (⟨⟨1, sorry⟩⟩ : Fin 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
-#check ⟨⟨1, sorry⟩⟩ -- expected type must be known
-#check (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
-#check (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
+#check_failure ⟨⟨1, sorry⟩⟩ -- expected type must be known
+#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
+#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat
 
 /-!
 As a final note, we can shorten the postponing act by using an additional

lean/main/09_tactics.lean

@@ -39,9 +39,10 @@ We start by simply declaring the tactic with no implementation:
 
 syntax "custom_tactic" : tactic
 
+/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
+#guard_msgs in --#
 example : 42 = 42 := by
   custom_tactic
--- tactic 'tacticCustom_tactic' has not been implemented
   sorry
 
 /-
@@ -60,11 +61,13 @@ example : 42 = 42 := by
 We can now try a harder problem, that cannot be immediately dispatched by `rfl`:
 -/
 
-example : 43 = 43 ∧ 42 = 42:= by
-  custom_tactic
--- tactic 'rfl' failed, equality expected
---   43 = 43 ∧ 42 = 42
--- ⊢ 43 = 43 ∧ 42 = 42
+#check_failure (by custom_tactic : 42 = 43 ∧ 42 = 42)
+-- type mismatch
+--   Iff.rfl
+-- has type
+--   ?m.1437 ↔ ?m.1437 : Prop
+-- but is expected to have type
+--   42 = 43 ∧ 42 = 42 : Prop
 
 /-
 We extend the `custom_tactic` tactic with a tactic that tries to break `And`
@@ -142,6 +145,7 @@ elab "custom_sorry_0" : tactic => do
 example : 1 = 2 := by
   custom_sorry_0
 -- unsolved goals: ⊢ 1 = 2
+  sorry
 
 /-
 This defines a syntax extension to Lean, where we are naming the piece of syntax
@@ -172,6 +176,7 @@ example : 1 = 2 := by
   custom_sorry_1
 -- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
 -- unsolved goals: ⊢ 1 = 2
+  sorry
 
 /-
 To `sorry` the goal, we can use the helper `Lean.Elab.admitGoal`:
@@ -242,13 +247,15 @@ example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
 -- H1 : 1 = 1
 -- H2 : 2 = 2
 -- ⊢ 2 = 2
+  sorry
 
 example (H1 : 1 = 1): 2 = 2 := by
   custom_assump_0
 -- goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
 -- unsolved goals
 -- H1 : 1 = 1
 -- ⊢ 2 = 2
+  sorry
 
 /-
 Next, we access the list of hypotheses, which are stored in a data structure
@@ -387,8 +394,7 @@ elab "custom_assump_2" : tactic =>
 example (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
   custom_assump_2
 
-example (H1 : 1 = 1): 2 = 2 := by
-  custom_assump_2
+#check_failure (by custom_assump_2 : (H1 : 1 = 1) → 2 = 2)
 -- tactic 'custom_assump_2' failed, unable to find matching hypothesis of type (2 = 2)
 -- H1 : 1 = 1
 -- ⊢ 2 = 2
@@ -466,6 +472,7 @@ theorem test_reverse_goals : (1 = 2 ∧ 3 = 4) ∧ 5 = 6 := by
 -- ⊢ 3 = 4
 -- case left.left
 -- ⊢ 1 = 2
+  all_goals sorry
 
 /-
 ## FAQ
@@ -571,16 +578,11 @@ elab "faq_throw_error" : tactic =>
     let goal ← Lean.Elab.Tactic.getMainGoal
     Lean.Meta.throwTacticEx `faq_throw_error goal "throwing an error at the current goal"
 
-example (b : Bool): b = true := by
-  cases b;
-  faq_throw_error
-  -- case true
-  -- ⊢ true = true
-  -- tactic 'faq_throw_error' failed, throwing an error at the current goal
-  -- case false
-  -- ⊢ false = true
+#check_failure (by faq_throw_error : (b : Bool) → b = true)
+-- tactic 'faq_throw_error' failed, throwing an error at the current goal
+-- ⊢ ∀ (b : Bool), b = true
 
-/-
+/-!
 **Q: What is the difference between `Lean.Elab.Tactic.*` and `Lean.Meta.Tactic.*`?**
 
 A: `Lean.Meta.Tactic.*` contains low level code that uses the `Meta` monad to