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

fix: isLevelDefEq missing case

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-25 10:27:14 -07:00
parent 0533fc4056
commit 675bebb446
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/LevelDefEq.lean
View file

@ -84,6 +84,7 @@ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
let ref ← getRef
let ctx ← read
trace[Meta.isLevelDefEq.stuck] "{lhs} =?= {rhs}"
modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := ref, ctx? := ctx.defEqCtx? }
mutual
@ -107,7 +108,9 @@ mutual
Bool.toLBool <$> isLevelDefEqAux levelZero v₂
| Level.zero _, Level.succ .. => return LBool.false
| Level.succ u _, v =>
if u.isMVar && u.occurs v then
if v.isParam then
return LBool.false
else if u.isMVar && u.occurs v then
return LBool.undef
else
match (← Meta.decLevel? v) with