From 8e860602f52a0e718478dc22beb267ef09e5aea1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <emilio@lean-fro.org>
Date: Mon, 9 Feb 2026 16:12:44 +0100
Subject: [PATCH] chore: remove unused variables warning showing up in build

Opted to fix the warnings instead of silencing them, except for the
case involving a mutual inductive.

I'm surprised by the behavior of the linter there, disabled warning
for now.
---
 test-projects/tutorial-test/TutorialExample/Data.lean   | 2 ++
 test-projects/tutorial-test/TutorialExample/RCases.lean | 4 ++--
 test-projects/website/DemoSite/Blog/Conditionals.lean   | 4 ++--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/test-projects/tutorial-test/TutorialExample/Data.lean b/test-projects/tutorial-test/TutorialExample/Data.lean
index af2a26ea..fb6f6a95 100644
--- a/test-projects/tutorial-test/TutorialExample/Data.lean
+++ b/test-projects/tutorial-test/TutorialExample/Data.lean
@@ -341,6 +341,8 @@ mutual
     | succ : Even n → Odd (n + 1)
 end
 
+set_option linter.unusedVariables false
+
 -- Trees with different node types
 mutual
   inductive TreeA (α : Type) where
diff --git a/test-projects/tutorial-test/TutorialExample/RCases.lean b/test-projects/tutorial-test/TutorialExample/RCases.lean
index b12d66d3..9c0b1c5b 100644
--- a/test-projects/tutorial-test/TutorialExample/RCases.lean
+++ b/test-projects/tutorial-test/TutorialExample/RCases.lean
@@ -487,8 +487,8 @@ example (h : ∃ n, P n) : True := by
   trivial
 
 -- Or just:
-example (h : ∃ n, P n) : True := by
-  trivial  -- h not needed at all
+example (_ : ∃ n, P n) : True := by
+  trivial  -- hypothesis not needed at all
 end
 ```
 
diff --git a/test-projects/website/DemoSite/Blog/Conditionals.lean b/test-projects/website/DemoSite/Blog/Conditionals.lean
index f565809d..6df394a8 100644
--- a/test-projects/website/DemoSite/Blog/Conditionals.lean
+++ b/test-projects/website/DemoSite/Blog/Conditionals.lean
@@ -153,7 +153,7 @@ Here's an inductive type and a structure:
 ```lean demo
 inductive A where
   | a1 | a2
-  | a3 (n : Nat)
+  | a3 : Nat → A
   | a4 : (n : Nat) → n = 3 → A
 
 structure S where
@@ -190,7 +190,7 @@ def quoted (str : String) : m Syntax := do
   let s ← `(a b c #[x, $(quote str), z])
   pure s
 
-example : ¬(quoted (m := m) = fun x => pure .missing) := by
+example : ¬(quoted (m := m) = fun _ => pure .missing) := by
   unfold quoted
   intro h
   let g : String → m Syntax := fun str => do