chore: fix explicitness of Option.mem_toList

2026-04-23 12:34:09 +00:00 · 2024-09-30 19:38:00 +10:00
1 changed files with 1 additions and 1 deletions
--- 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