fix plural

leanprover · Nov 5, 2024 · 40291d6 · 40291d6
1 parent 7893618
commit 40291d6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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 =>