From 093ab49b7fd1ff903f0347328e70febdbff08686 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Mar 2022 11:58:47 -0800
Subject: [PATCH] feat: improve `generateElements` a bit

---
 src/Lean/Elab/PreDefinition/WF/Rel.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 5575d0237c..217bb2a353 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -111,6 +111,7 @@ where
   generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do
     let mut result := #[]
     let var ← `(x)
+    let body ← `(sizeOf x)
     let hole ← `(_)
     for preDef in preDefs, numArg in numArgs, argIdx in argCombination do
       let mut vars := #[var]
@@ -120,7 +121,7 @@ where
         ref := preDef.ref
         declName := preDef.declName
         vars := vars
-        body := var
+        body := body
         implicit := false
       }
     return result