From 3e0a975e9c67c8ed6bb2f4b6280404bb364a58d9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Apr 2022 08:37:34 -0700 Subject: [PATCH] chore: fix test --- tests/lean/run/dotNameIssue.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/dotNameIssue.lean b/tests/lean/run/dotNameIssue.lean index 5198e509f9..df334dcacf 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