fix: (throwaway) context was ignoring const levels

leanprover · Nov 7, 2019 · 8992fe1 · 8992fe1
1 parent 06fe9d3
commit 8992fe1
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean
@@ -282,7 +282,9 @@ partial def uAlphaNormalizeCore : Level → StateM AlphaNormData Level
 
 partial def eAlphaNormalizeCore : Expr → StateM AlphaNormData Expr
 | e =>
-  if e.isConst then pure e
+  if e.isConst then do
+    ls ← e.constLevels!.mapM uAlphaNormalizeCore;
+    pure $ Expr.updateConst! e ls
   else if e.isFVar then pure e
   else if !e.hasMVar then pure e
   else match e with