Equations
- Lean.Meta.clear mvarId fvarId = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `clear let lctx ← Lean.getLCtx let _do_jp : PUnit → Lean.MetaM Lean.MVarId := fun y => do let tag ← Lean.Meta.getMVarTag mvarId let mctx ← Lean.getMCtx Lean.LocalContext.forM lctx fun localDecl => if (Lean.LocalDecl.fvarId localDecl == fvarId) = true then pure PUnit.unit else if Lean.MetavarContext.localDeclDependsOn mctx localDecl fvarId = true then Lean.Meta.throwTacticEx `clear mvarId (Lean.toMessageData "variable '" ++ Lean.toMessageData (Lean.LocalDecl.toExpr localDecl) ++ Lean.toMessageData "' depends on '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'") Lean.Syntax.missing else pure PUnit.unit let mvarDecl ← Lean.Meta.getMVarDecl mvarId let _do_jp : PUnit → Lean.MetaM Lean.MVarId := fun y => let lctx := Lean.LocalContext.erase lctx fvarId; do let localInsts ← Lean.Meta.getLocalInstances let localInsts : Lean.LocalInstances := match Array.findIdx? localInsts fun localInst => Lean.Expr.fvarId! localInst.fvar == fvarId with | none => localInsts | some idx => Array.eraseIdx localInsts idx let newMVar ← Lean.Meta.mkFreshExprMVarAt lctx localInsts mvarDecl.type Lean.MetavarKind.syntheticOpaque tag 0 Lean.Meta.assignExprMVar mvarId newMVar pure (Lean.Expr.mvarId! newMVar) if Lean.MetavarContext.exprDependsOn mctx mvarDecl.type fvarId = true then do let y ← Lean.Meta.throwTacticEx `clear mvarId (Lean.toMessageData "target depends on '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y if Lean.LocalContext.contains lctx fvarId = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `clear mvarId (Lean.toMessageData "unknown variable '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'") Lean.Syntax.missing _do_jp y
Equations
- Lean.Meta.tryClear mvarId fvarId = HOrElse.hOrElse (Lean.Meta.clear mvarId fvarId) fun x => pure mvarId
Equations
- Lean.Meta.tryClearMany mvarId fvarIds = Array.foldrM (fun fvarId mvarId => Lean.Meta.tryClear mvarId fvarId) mvarId fvarIds (Array.size fvarIds)