From d4219c9d705259b79c99f51628e155b6aa30ccf6 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 8 Oct 2022 21:25:27 -0400 Subject: [PATCH] fix: `List.Mem` should have two parameters --- src/Init/Data/List/Basic.lean | 6 +++--- tests/lean/run/dotNameIssue.lean | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index f15f9b6179..6af96a1e5b 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -240,9 +240,9 @@ def notElem [BEq α] (a : α) (as : List α) : Bool := abbrev contains [BEq α] (as : List α) (a : α) : Bool := elem a as -inductive Mem : α → List α → Prop - | head (a : α) (as : List α) : Mem a (a::as) - | tail (a : α) {b : α} {as : List α} : Mem b as → Mem b (a::as) +inductive Mem (a : α) : List α → Prop + | head (as : List α) : Mem a (a::as) + | tail (b : α) {as : List α} : Mem a as → Mem a (b::as) instance : Membership α (List α) where mem := Mem diff --git a/tests/lean/run/dotNameIssue.lean b/tests/lean/run/dotNameIssue.lean index df334dcacf..5198e509f9 100644 --- a/tests/lean/run/dotNameIssue.lean +++ b/tests/lean/run/dotNameIssue.lean @@ -1,7 +1,7 @@ example : x ≠ y → x ∉ [y] := fun hne hin => match hin with - | .head _ _ => hne rfl + | .head _ => hne rfl example : x ≠ y → x ∉ [y] := - fun hne (.head _ _) => hne rfl + fun hne (.head _) => hne rfl