From 971a2d7da5d3a9cc3859013980c7ae43152874df Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Wed, 5 Feb 2025 03:19:37 +0900
Subject: [PATCH] message assertion

---
 lean/main/05_syntax.lean  | 63 ++++++++++++++++++++++++---------------
 lean/main/06_macros.lean  |  4 ++-
 lean/main/09_tactics.lean | 55 +++++++++++++++++++++-------------
 3 files changed, 76 insertions(+), 46 deletions(-)

diff --git a/lean/main/05_syntax.lean b/lean/main/05_syntax.lean
index 2828933..6961c9e 100644
--- a/lean/main/05_syntax.lean
+++ b/lean/main/05_syntax.lean
@@ -18,18 +18,18 @@ import Lean
 -- XOR, denoted \oplus
 infixl:60 " ⊕ " => fun l r => (!l && r) || (l && !r)
 
-#eval true ⊕ true -- false
-#eval true ⊕ false -- true
-#eval false ⊕ true -- true
-#eval false ⊕ false -- false
+#guard !(true ⊕ true)
+#guard true ⊕ false
+#guard false ⊕ true
+#guard !(false ⊕ false)
 
 -- with `notation`, "left XOR"
 notation:10 l:10 " LXOR " r:11 => (!l && r)
 
-#eval true LXOR true -- false
-#eval true LXOR false -- false
-#eval false LXOR true -- true
-#eval false LXOR false -- false
+#guard !(true LXOR true)
+#guard !(true LXOR false)
+#guard false LXOR true
+#guard !(false LXOR false)
 
 /- As we can see the `infixl` command allows us to declare a notation for
 a binary operation that is infix, meaning that the operator is in between
@@ -52,9 +52,9 @@ The two unintuitive parts about these two are:
   precedence, meaning how strong they bind to their arguments, let's see this in action:
 -/
 
-#eval true ⊕ false LXOR false -- false
-#eval (true ⊕ false) LXOR false -- false
-#eval true ⊕ (false LXOR false) -- true
+#guard !(true ⊕ false LXOR false)
+#guard !((true ⊕ false) LXOR false)
+#guard true ⊕ (false LXOR false)
 
 /-!
 As we can see, the Lean interpreter analyzed the first term without parentheses
@@ -154,9 +154,12 @@ 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:
 -/
 
+/-⋆-//--
+info: elaboration function for 'termMyTerm' has not been implemented
+  MyTerm
+-/
+#guard_msgs in --#
 #check_failure MyTerm
--- elaboration function for 'termMyTerm' has not been implemented
---   MyTerm
 
 /-! Note: `#check_failure` command allows incorrectly typed terms to be indicated without error. -/
 
@@ -276,13 +279,20 @@ 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:
+-/
+
+open Lean Parser in
+/-- function to check if parsing passes -/
+def parse (cat : Name) (s : String) : MetaM Syntax := do
+  ofExcept <| runParserCategory (← getEnv) cat s
 
-```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'
-```
--/
+#check_failure bin(Z, O, Z, Z, O) -- elaboration function hasn't been implemented but parsing passes
+
+-- fails to parse `bin()` because `binNumber` is "one or many": expected 'O' or 'Z'
+/-⋆-//-- error: <input>:1:4: expected 'O' or 'Z' -/
+#guard_msgs in --#
+#eval parse `term "bin()"
 
 syntax binNumber' := binDigit,* -- note the *
 syntax "emptyBin(" binNumber' ")" : term
@@ -390,8 +400,8 @@ def isAdd11 : Syntax → Bool
   | `(Nat.add 1 1) => true
   | _ => false
 
-#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- true
-#eval isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- false
+#guard isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- true
+#guard ! isAdd11 (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- false
 
 /-!
 The next level with matches is to capture variables from the input instead
@@ -426,8 +436,8 @@ def isLitAdd : TSyntax `term → Option Nat
   | `(Nat.add $x:num $y:num) => some (x.getNat + y.getNat)
   | _ => none
 
-#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) -- some 2
-#eval isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) -- none
+#guard isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "1", Syntax.mkNumLit "1"]) = some 2
+#guard isLitAdd (Syntax.mkApp (mkIdent `Nat.add) #[mkIdent `foo, Syntax.mkNumLit "1"]) = none
 
 /-!
 If you want to access the `Syntax` behind a `TSyntax` you can do this using
@@ -448,6 +458,7 @@ chapters.
 declare_syntax_cat arith
 
 syntax num : arith
+
 syntax arith "-" arith : arith
 syntax arith "+" arith : arith
 syntax "(" arith ")" : arith
@@ -466,7 +477,9 @@ def test : Elab.TermElabM Nat := do
   let stx ← `(arith| (12 + 3) - 4)
   pure (denoteArith stx)
 
-#eval test -- 11
+/-⋆-//-- info: 11 -/
+#guard_msgs in --#
+#eval test
 
 /-!
 Feel free to play around with this example and extend it in whatever way
@@ -547,7 +560,9 @@ basic version of our notation:
 -/
 notation "{ " x " | " p " }" => setOf (fun x => p)
 
-#check { (x : Nat) | x ≤ 1 } -- { x | x ≤ 1 } : Set Nat
+/-⋆-//-- info: { x | x ≤ 1 } : Set Nat -/
+#guard_msgs in --#
+#check { (x : Nat) | x ≤ 1 }
 
 example : 1 ∈ { (y : Nat) | y ≤ 1 } := by simp[Membership.mem, Set.mem, setOf]
 example : 2 ∈ { (y : Nat) | y ≤ 3 ∧ 1 ≤ y } := by simp[Membership.mem, Set.mem, setOf]
diff --git a/lean/main/06_macros.lean b/lean/main/06_macros.lean
index c3323fa..8004eec 100644
--- a/lean/main/06_macros.lean
+++ b/lean/main/06_macros.lean
@@ -154,7 +154,9 @@ compiler, you could also declare functions that are specific to certain
 `TSyntax` variants. For example as we have seen in the syntax chapter
 there exists the function:
 -/
-#check TSyntax.getNat -- TSyntax.getNat : TSyntax numLitKind → Nat
+/-⋆-//-- info: Lean.TSyntax.getNat (s : NumLit) : Nat -/
+#guard_msgs in
+#check TSyntax.getNat
 /-!
 Which is guaranteed to not panic because we know that the `Syntax` that
 the function is receiving is a numeric literal and can thus naturally
diff --git a/lean/main/09_tactics.lean b/lean/main/09_tactics.lean
index 5cd7a1a..b637fd8 100644
--- a/lean/main/09_tactics.lean
+++ b/lean/main/09_tactics.lean
@@ -39,11 +39,10 @@ We start by simply declaring the tactic with no implementation:
 
 syntax "custom_tactic" : tactic
 
-/-- error: tactic 'tacticCustom_tactic' has not been implemented -/
+/-⋆-//-- error: tactic 'tacticCustom_tactic' has not been implemented -/
 #guard_msgs in --#
 example : 42 = 42 := by
   custom_tactic
-  sorry
 
 /-
 We will now add the `rfl` tactic into `custom_tactic`, which will allow us to
@@ -54,20 +53,23 @@ macro_rules
 | `(tactic| custom_tactic) => `(tactic| rfl)
 
 example : 42 = 42 := by
-   custom_tactic
--- Goals accomplished 🎉
+  custom_tactic
+  -- Goals accomplished 🎉
 
 /-
 We can now try a harder problem, that cannot be immediately dispatched by `rfl`:
 -/
 
-#check_failure (by custom_tactic : 43 = 43 ∧ 42 = 42)
--- type mismatch
---   Iff.rfl
--- has type
---   ?m.1437 ↔ ?m.1437 : Prop
--- but is expected to have type
---   43 = 43 ∧ 42 = 42 : Prop
+/-⋆-//--
+error: tactic 'rfl' failed, the left-hand side
+  43 = 43
+is not definitionally equal to the right-hand side
+  42 = 42
+⊢ 43 = 43 ∧ 42 = 42
+-/
+#guard_msgs in --#
+example : 43 = 43 ∧ 42 = 42 := by
+  custom_tactic
 
 /-
 We extend the `custom_tactic` tactic with a tactic that tries to break `And`
@@ -89,7 +91,7 @@ that we dispatch the theorem.
 
 example : 43 = 43 ∧ 42 = 42 := by
   custom_tactic
--- Goals accomplished 🎉
+  -- Goals accomplished 🎉
 
 /-
 In summary, we declared an extensible tactic called `custom_tactic`. It
@@ -120,9 +122,12 @@ macro_rules
 theorem test_and_then: 1 = 1 ∧ 2 = 2 := by
   apply And.intro and_then rfl
 
+/-⋆-//--
+info: theorem test_and_then : 1 = 1 ∧ 2 = 2 :=
+⟨Eq.refl 1, Eq.refl 2⟩
+-/
+#guard_msgs in --#
 #print test_and_then
--- theorem test_and_then : 1 = 1 ∧ 2 = 2 :=
--- { left := Eq.refl 1, right := Eq.refl 2 }
 
 /-
 ## Exploring `TacticM`
@@ -394,10 +399,14 @@ elab "custom_assump_2" : tactic =>
 example (H1 : 1 = 1) (H2 : 2 = 2) : 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
+/-⋆-//--
+error: tactic 'custom_assump_2' failed, unable to find matching hypothesis of type (2 = 2)
+H1 : 1 = 1
+⊢ 2 = 2
+-/
+#guard_msgs in --#
+example (H1 : 1 = 1) : 2 = 2 := by
+  custom_assump_2
 
 /-
 ### Tweaking the context
@@ -578,9 +587,13 @@ 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"
 
-#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
+/-⋆-//--
+error: tactic 'faq_throw_error' failed, throwing an error at the current goal
+⊢ ∀ (b : Bool), b = true
+-/
+#guard_msgs in --#
+example : (b : Bool) → b = true := by
+  faq_throw_error
 
 /-!
 **Q: What is the difference between `Lean.Elab.Tactic.*` and `Lean.Meta.Tactic.*`?**