Make a nit

AeneasVerif · Feb 25, 2025 · 1bca2a4 · 1bca2a4
1 parent d4ad011
commit 1bca2a4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/backends/lean/Aeneas/BvTac/BvTac.lean b/backends/lean/Aeneas/BvTac/BvTac.lean
@@ -19,7 +19,7 @@ partial def getn : TacticM Expr := do
   let raiseError : TacticM Expr :=
     throwError "The goal doesn't have the proper shape: expected a proposition only involving (in-)equality between bitvectors"
   let fromBitVecTy (ty : Expr) : TacticM Expr :=
-    ty.consumeMData.withApp fun f args => do
+    ty.consumeMData.withApp fun _ args => do
     if args.size == 1 then
       pure args[0]!
     else