chore: fix explicitness of Option.mem_toList (#5539)

leanprover · Sep 30, 2024 · 6bd0d9d · 6bd0d9d
1 parent db79d9e
commit 6bd0d9d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean
@@ -8,7 +8,7 @@ import Init.Data.List.Lemmas
 
 namespace Option
 
-@[simp] theorem mem_toList (a : α) (o : Option α) : a ∈ o.toList ↔ a ∈ o := by
+@[simp] theorem mem_toList {a : α} {o : Option α} : a ∈ o.toList ↔ a ∈ o := by
   cases o <;> simp [eq_comm]
 
 end Option