From 40291d6f498d9559c9fa039942bc31f041007a68 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 5 Nov 2024 12:31:27 -0800 Subject: [PATCH] fix plural --- src/Lean/Elab/Tactic/Conv/Congr.lean | 2 +- tests/lean/run/conv_arg.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 407b62a65f0b..08eb606d991e 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -200,7 +200,7 @@ where if explicit then let i := if i > 0 then i - 1 else i + xs.size if i < 0 || i ≥ xs.size then - throwError "invalid '{tacticName}' tactic, application has {xs.size} arguments but the index is out of bounds" + throwError "invalid '{tacticName}' tactic, application has {xs.size} argument(s) but the index is out of bounds" let idx := i.natAbs return (mkAppN f xs[0:idx], xs[idx:]) else diff --git a/tests/lean/run/conv_arg.lean b/tests/lean/run/conv_arg.lean index c9237f09bee0..6e6cf576bbbc 100644 --- a/tests/lean/run/conv_arg.lean +++ b/tests/lean/run/conv_arg.lean @@ -73,7 +73,7 @@ example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by conv => enter [1, 6] -/-- error: invalid 'arg' tactic, application has 2 arguments but the index is out of bounds -/ +/-- error: invalid 'arg' tactic, application has 2 argument(s) but the index is out of bounds -/ #guard_msgs in example (f : {_ : Nat} → Nat → Nat) (h : m = m') : @f n m = @f n m' := by conv =>