Use fine-grained equations for non-rec equations

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -75,6 +75,9 @@ private def findMatchToSplit? (env : Environment) (e : Expr) (declNames : Array
           break
       unless hasFVarDiscr do
         return Expr.FindStep.visit
+      -- Hack: if `declNames` is empty, skip this check. To be revisited:
+      if declNames.isEmpty then
+          return Expr.FindStep.found
       -- At least one alternative must contain a `declNames` application with loose bound variables.
       for i in [info.getFirstAltPos : info.getFirstAltPos + info.numAlts] do
         let alt := args[i]!

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -10,6 +10,7 @@ import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Eqns
 import Lean.Meta.ArgsPacker.Basic
 import Init.Data.Array.Basic
+import Lean.Elab.PreDefinition.Nonrec.Eqns -- imported here to ensure it registers first
 
 namespace Lean.Elab.WF
 open Meta

tests/lean/run/reserved.lean

@@ -50,17 +50,14 @@ info: nonrecfun.eq_def :
 #guard_msgs in
 #check nonrecfun.eq_def
 
-/--
-info: nonrecfun.eq_1 :
-  ∀ (x : Bool),
-    nonrecfun x =
-      match x with
-      | false => 0
-      | true => 0
--/
+/-- info: nonrecfun.eq_1 : nonrecfun false = 0 -/
 #guard_msgs in
 #check nonrecfun.eq_1
 
+/-- info: nonrecfun.eq_2 : nonrecfun true = 0 -/
+#guard_msgs in
+#check nonrecfun.eq_2
+
 def fact : Nat → Nat
   | 0 => 1
   | n+1 => (n+1) * fact n
@@ -130,3 +127,10 @@ info: find.eq_def (as : Array Int) (i : Nat) (v : Int) :
 -/
 #guard_msgs in
 #check find.eq_def
+
+/--
+info: find.eq_1 (as : Array Int) (i : Nat) (v : Int) :
+  find as i v = if x : i < as.size then if as[i] = v then i else find as (i + 1) v else i
+-/
+#guard_msgs in
+#check find.eq_1