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

fix: infinite loop in isClassApp?

Browse source
This commit is contained in:
Mario Carneiro 2023-05-30 08:20:57 -04:00 • committed by Leonardo de Moura
parent 5661b15e35
commit 9ec9ea61a4
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Basic.lean
View file

@ -986,7 +986,7 @@ mutual
-- Helper method for isClassExpensive?
private partial def isClassApp? (type : Expr) : MetaM (Option Name) := do
private partial def isClassApp? (type : Expr) (instantiated := false) : MetaM (Option Name) := do
match type.getAppFn with
| .const c _ =>
let env ← getEnv
@ -997,7 +997,9 @@ mutual
match (← whnf type).getAppFn with
| .const c _ => if isClass env c then return some c else return none
| _ => return none
| .mvar .. => isClassApp? (← instantiateMVars type)
| .mvar .. =>
if instantiated then return none
isClassApp? (← instantiateMVars type) true
| _ => return none
private partial def isClassExpensive? (type : Expr) : MetaM (Option Name) :=