chore: unused variable warnings (#52)

leanprover · Oct 11, 2024 · 313a82f · 313a82f
1 parent 505974b
commit 313a82f
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Tests.lean b/Tests.lean
@@ -45,7 +45,7 @@ def heya : IO Unit := do
   if x == 3 /-
     !! begin foo
   -/ || true /- !! end foo -/ then pure ()
-  let x := [1, 2/- !! begin foo-/, 3/- !! end foo-/]
+  let _ := [1, 2/- !! begin foo-/, 3/- !! end foo-/]
   pure ()
 
 def expectedLog :=

diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -93,7 +93,7 @@ instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
       ⟨(x, y)⟩
 
 
-example [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : Inhabited (m (Nat × α × Nat)) := inferInstance
+example [Inhabited α] [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (_ : α) : Inhabited (m (Nat × α × Nat)) := inferInstance
 
 -- Lifted from find's where block to make sure the Inhabited instance is found
 partial def find.loop [Inhabited α] [Monad m] [MonadState (State α) m] (i : Nat) : m (Nat × α × Nat) := do