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