compiling more quietly now

leanprover-community · Oct 14, 2023 · a8ad0f3 · a8ad0f3
1 parent aa6bb6d
commit a8ad0f3
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/Game/Levels/AdvAddition/L01ne_succ_self.lean b/Game/Levels/AdvAddition/L01ne_succ_self.lean
@@ -15,6 +15,9 @@ which is a warm-up to see if you remember `zero_ne_succ`
 and `succ_inj`, and how to use the `apply` tactic.
 "
 
+LemmaDoc MyNat.ne_succ_self as "ne_succ_self" in "≤" "
+`ne_succ_self n` is the proof that `n ≠ succ n`."
+
 /-- $n\neq\operatorname{succ}(n)$. -/
 Statement ne_succ_self (n : ℕ) : n ≠ succ n := by
   Hint "Start with `induction`."

diff --git a/Game/Levels/Implication/L01exact.lean b/Game/Levels/Implication/L01exact.lean
@@ -45,6 +45,11 @@ the hypotheses.
 "
 
 /-- Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$. -/
+/-
+When buildint this generates a warning
+unused variable `h2` [linter.unusedVariables]
+but I want `h2` to be there.
+-/
 Statement (x y z : ℕ) (h1 : x + y = 37) (h2 : 3 * x + z = 42) : x + y = 37 := by
   Hint "The goal is one of our hypotheses. Solve the goal by executing `exact h1`."
   exact h1