max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve test at packDomain

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-09 10:01:42 -08:00
parent e66575d4fc
commit 471ef75345
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/PreDefinition/WF/PackDomain.lean
View file

@ -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 }