fix: expandTerminationByNonCore

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

@@ -139,7 +139,7 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
       if let some missing := clique.find? fun declName => elements.find? (·.declName == declName) |>.isNone then
         withRef elements[0].ref <| Macro.throwError s!"invalid `termination_by` syntax, missing case for function '{missing}'"
       result := result.push { elements }
-  unless usedElse do
+  if !usedElse && elseElemStx?.isSome then
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
   return TerminationBy.ext result
 

tests/lean/run/mutwf1.lean

@@ -1,4 +1,4 @@
--- set_option trace.Elab.definition.wf true in
+namespace Ex1
 mutual
   def f : Nat → α → α → α
     | 0, a, b => a
@@ -25,3 +25,30 @@ termination_by'
 #print h
 
 #eval f 5 'a' 'b'
+end Ex1
+
+namespace Ex2
+mutual
+  def f : Nat → α → α → α
+    | 0, a, b => a
+    | n, a, b => g a n b |>.1
+
+  def g : α → Nat → α → (α × α)
+    | a, 0, b => (a, b)
+    | a, n, b => (h a b n, a)
+
+  def h : α → α → Nat → α
+    | a, b, 0 => b
+    | a, b, n+1 => f n a b
+end
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
+
+#print f
+#print g
+#print h
+
+#eval f 5 'a' 'b'
+end Ex2

tests/lean/run/mutwf4.lean

@@ -11,13 +11,9 @@ mutual
     else
       n
 end
-termination_by'
-  invImage
-    (fun
-     | Sum.inl ⟨n, true⟩ => (n, 2)
-     | Sum.inl ⟨n, false⟩ => (n, 1)
-     | Sum.inr n => (n, 0))
-  $ Prod.lex sizeOfWFRel sizeOfWFRel
+termination_by
+  f n b => (n, if b then 2 else 1)
+  g n   => (n, 0)
 
 #print f
 #print g