chore: fix typo in trace.split.failure error message (leanprover#4431)

should be "failure" not "failures" Co-authored-by: q r <[email protected]>
leanprover · Jun 12, 2024 · bedcbfc · bedcbfc
1 parent ce6ebd1
commit bedcbfc
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean
@@ -21,20 +21,20 @@ open Meta
       throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
     if simplifyTarget then
       liftMetaTactic fun mvarId => do
-       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`"
+       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`"
         return mvarIds
     else
       let fvarId ← getFVarId hyps[0]!
       liftMetaTactic fun mvarId => do
-        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`"
+        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`"
         return mvarIds
   | Location.wildcard =>
     liftMetaTactic fun mvarId => do
       let fvarIds ← mvarId.getNondepPropHyps
       for fvarId in fvarIds do
         if let some mvarIds ← splitLocalDecl? mvarId fvarId then
           return mvarIds
-      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failures true`"
+      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId "consider using `set_option trace.split.failure true`"
       return mvarIds
 
 end Lean.Elab.Tactic
diff --git a/tests/lean/run/4390.lean b/tests/lean/run/4390.lean
@@ -11,7 +11,7 @@ termination_by state
 decreasing_by sorry
 
 /--
-error: tactic 'split' failed, consider using `set_option trace.split.failures true`
+error: tactic 'split' failed, consider using `set_option trace.split.failure true`
 state : Nat
 p :
   (match h : step state with