Equations
- Lean.Meta.isLevelDefEqAuxImpl x x = match x, x with | Lean.Level.succ lhs x, Lean.Level.succ rhs x_1 => Lean.Meta.isLevelDefEqAux lhs rhs | lhs, rhs => if (Lean.Level.getLevelOffset lhs == Lean.Level.getLevelOffset rhs) = true then pure (Lean.Level.getOffset lhs == Lean.Level.getOffset rhs) else let cls := `Meta.isLevelDefEq.step; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => do let lhs' ← Lean.Meta.instantiateLevelMVars lhs let lhs' : Lean.Level := Lean.Level.normalize lhs' let rhs' ← Lean.Meta.instantiateLevelMVars rhs let rhs' : Lean.Level := Lean.Level.normalize rhs' if (lhs != lhs' || rhs != rhs') = true then Lean.Meta.isLevelDefEqAux lhs' rhs' else do let r ← Lean.Meta.solve lhs rhs if (r != Lean.LBool.undef) = true then pure (r == Lean.LBool.true) else do let r ← Lean.Meta.solve rhs lhs if (r != Lean.LBool.undef) = true then pure (r == Lean.LBool.true) else do let mctx ← Lean.getMCtx if (!Lean.MetavarContext.hasAssignableLevelMVar mctx lhs && !Lean.MetavarContext.hasAssignableLevelMVar mctx rhs) = true then do let ctx ← read if (ctx.config.isDefEqStuckEx && (Lean.Level.isMVar lhs || Lean.Level.isMVar rhs)) = true then let cls := `Meta.isLevelDefEq.stuck; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => Lean.Meta.throwIsDefEqStuck if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lhs ++ Lean.toMessageData " =?= " ++ Lean.toMessageData rhs ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y else pure false else do Lean.Meta.postponeIsLevelDefEq lhs rhs pure true if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData lhs ++ Lean.toMessageData " =?= " ++ Lean.toMessageData rhs ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y