From 471ef75345eee9bcbe8563060382b323c99ddb57 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 9 Feb 2022 10:01:42 -0800 Subject: [PATCH] feat: improve test at `packDomain` --- src/Lean/Elab/PreDefinition/WF/PackDomain.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean index dd4d1caa24..ee17caead5 100644 --- a/src/Lean/Elab/PreDefinition/WF/PackDomain.lean +++ b/src/Lean/Elab/PreDefinition/WF/PackDomain.lean @@ -115,7 +115,11 @@ def packDomain (preDefs : Array PreDefinition) : MetaM (Array PreDefinition) := else return TransformStep.done e mkLambdaFVars #[y] (← transform newBody (post := visit)) - if let some bad := valueNew.find? fun e => (isAppOfPreDef? e).isSome && e.getAppNumArgs > 1 then + let isBad (e : Expr) : Bool := + match isAppOfPreDef? e with + | none => false + | some i => e.getAppNumArgs > 1 || preDefsNew[i].declName != preDefs[i].declName + if let some bad := valueNew.find? isBad then if let some i := isAppOfPreDef? bad then throwErrorAt preDef.ref "well-founded recursion cannot be used, function '{preDef.declName}' contains application of function '{preDefs[i].declName}' with #{bad.getAppNumArgs} argument(s), but function has arity {arities[i]}" preDefsNew := preDefsNew.set! i { preDefNew with value := valueNew }