Equations
- Lean.Meta.cleanup mvarId = (fun addUsedFVars addUsedFVar collectProps collectUsed => Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `cleanup let used ← StateRefT'.run' collectUsed (false, ∅) let lctx ← Lean.getLCtx let r ← forIn lctx lctx fun localDecl r => let lctx := r; if Std.RBTree.contains used (Lean.LocalDecl.fvarId localDecl) = true then do pure PUnit.unit pure (ForInStep.yield lctx) else let lctx := Lean.LocalContext.erase lctx (Lean.LocalDecl.fvarId localDecl); do pure PUnit.unit pure (ForInStep.yield lctx) let x : Lean.LocalContext := r let lctx : Lean.LocalContext := x let a ← Lean.Meta.getLocalInstances let localInsts : Array Lean.LocalInstance := Array.filter (fun inst => Std.RBTree.contains used (Lean.Expr.fvarId! inst.fvar)) a 0 (Array.size a) let a ← Lean.Meta.getMVarType mvarId let a ← Lean.Meta.instantiateMVars a let a_1 ← Lean.Meta.getMVarTag mvarId let mvarNew ← Lean.Meta.mkFreshExprMVarAt lctx localInsts a Lean.MetavarKind.syntheticOpaque a_1 0 Lean.Meta.assignExprMVar mvarId mvarNew pure (Lean.Expr.mvarId! mvarNew)) Lean.Meta.cleanup.addUsedFVars Lean.Meta.cleanup.addDeps Lean.Meta.cleanup.addUsedFVar Lean.Meta.cleanup.collectPropsStep Lean.Meta.cleanup.collectProps (Lean.Meta.cleanup.collectUsed mvarId)
Equations
- Lean.Meta.cleanup.collectPropsStep = do let a ← get let usedSet : Lean.FVarIdSet := a.snd let a ← Lean.getLCtx let r ← let col := a; forIn col PUnit.unit fun localDecl r => do let a ← liftM (Lean.Meta.isProp (Lean.LocalDecl.type localDecl)) if a = true then do let a ← liftM (Lean.Meta.dependsOnPred (Lean.LocalDecl.type localDecl) (Std.RBTree.contains usedSet)) if a = true then do Lean.Meta.cleanup.addUsedFVar (Lean.LocalDecl.fvarId localDecl) pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r pure PUnit.unit
Equations
- Lean.Meta.cleanup.collectUsed mvarId = do let a ← liftM (Lean.Meta.getMVarType' mvarId) Lean.Meta.cleanup.addUsedFVars a Lean.Meta.cleanup.collectProps let a ← get pure a.snd