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

fix: levelMVarToParam consider Expr assignment

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-22 13:55:04 -07:00
parent be4d65e936
commit fe5a0026cd
2 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Inductive.lean
View file

@ -250,11 +250,9 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
`inferResultingUniverse`. -/
private def levelMVarToParamAux (ref : Syntax) (indTypes : List InductiveType) : StateT Nat TermElabM (List InductiveType) :=
indTypes.mapM fun indType => do
type ← liftM $ Term.instantiateMVars ref indType.type;
type ← Term.levelMVarToParam' type;
type ← Term.levelMVarToParam' indType.type;
ctors ← indType.ctors.mapM fun ctor => do {
ctorType ← liftM $ Term.instantiateMVars ref ctor.type;
ctorType ← Term.levelMVarToParam' ctorType;
ctorType ← Term.levelMVarToParam' ctor.type;
pure { ctor with type := ctorType }
};
pure { indType with ctors := ctors, type := type }

7
src/Lean/MetavarContext.lean
View file

@ -1011,7 +1011,7 @@ partial def visitLevel : Level → M Level
pure p
@[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
if e.hasLevelMVar then f e else pure e
if e.hasMVar then f e else pure e
partial def main : Expr → M Expr
| e@(Expr.proj _ _ s _) => do s ← visit main s; pure (e.updateProj! s)
@ -1022,6 +1022,11 @@ partial def main : Expr → M Expr
| e@(Expr.mdata _ b _) => do b ← visit main b; pure (e.updateMData! b)
| e@(Expr.const _ us _) => do us ← us.mapM visitLevel; pure (e.updateConst! us)
| e@(Expr.sort u _) => do u ← visitLevel u; pure (e.updateSort! u)
| e@(Expr.mvar mvarId _) => do
s ← get;
match s.mctx.getExprAssignment? mvarId with
| some v => visit main v
| none => pure e
| e => pure e
end LevelMVarToParam