fix plural

Author: kmill

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

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 =>