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

chore: tc: only normalize level mvars at current depth

Browse source
This commit is contained in:
Gabriel Ebner 2022-12-21 10:46:52 -08:00
parent e71a2e58bb
commit f798507bbf
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/SynthInstance.lean
View file

@ -102,7 +102,7 @@ partial def normLevel (u : Level) : M Level := do
| Level.max v w => return u.updateMax! (← normLevel v) (← normLevel w)
| Level.imax v w => return u.updateIMax! (← normLevel v) (← normLevel w)
| Level.mvar mvarId =>
if !(← isLevelMVarAssignable mvarId) then
if (← getMCtx).getLevelDepth mvarId != (← getMCtx).depth then
return u
else
let s ← get