def
Lean.Meta.revert
(mvarId : Lean.MVarId)
(fvarIds : Array Lean.FVarId)
(preserveOrder : optParam Bool false)
:
Equations
- Lean.Meta.revert mvarId fvarIds preserveOrder = if Array.isEmpty fvarIds = true then pure (#[], mvarId) else Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `revert let r ← forIn fvarIds PUnit.unit fun fvarId r => do let a ← Lean.Meta.getLocalDecl fvarId if Lean.LocalDecl.isAuxDecl a = true then do Lean.throwError (Lean.toMessageData "failed to revert " ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData ", it is an auxiliary declaration created to represent recursive definitions") pure (ForInStep.yield PUnit.unit) else do pure PUnit.unit pure (ForInStep.yield PUnit.unit) let x : PUnit := r let fvars : Array Lean.Expr := Array.map Lean.mkFVar fvarIds let a ← Lean.getMCtx let a_1 ← Lean.getLCtx match Lean.MetavarContext.MkBinding.collectDeps a a_1 fvars preserveOrder with | Except.error x => Lean.throwError (Lean.toMessageData "failed to revert variables " ++ Lean.toMessageData fvars ++ Lean.toMessageData "") | Except.ok toRevert => let mvarId := mvarId; let toRevertNew := #[]; do let r ← forIn toRevert { fst := toRevertNew, snd := mvarId } fun x r => let toRevertNew := r.fst; let mvarId := r.snd; do let a ← Lean.Meta.getLocalDecl (Lean.Expr.fvarId! x) if Lean.LocalDecl.isAuxDecl a = true then do let r ← Lean.Meta.clear mvarId (Lean.Expr.fvarId! x) let mvarId : Lean.MVarId := r pure PUnit.unit pure (ForInStep.yield { fst := toRevertNew, snd := mvarId }) else let toRevertNew := Array.push toRevertNew x; do pure PUnit.unit pure (ForInStep.yield { fst := toRevertNew, snd := mvarId }) let x : MProd (Array Lean.Expr) Lean.MVarId := r match x with | { fst := toRevertNew, snd := mvarId } => do let tag ← Lean.Meta.getMVarTag mvarId Lean.Meta.setMVarKind mvarId Lean.MetavarKind.natural let _do_jp : Lean.Expr × Array Lean.Expr → Lean.MetaM (Array Lean.FVarId × Lean.MVarId) := fun discr => let x := discr; match x with | (e, toRevert) => let mvar := Lean.Expr.getAppFn e; do Lean.Meta.setMVarTag (Lean.Expr.mvarId! mvar) tag pure (Array.map Lean.Expr.fvarId! toRevert, Lean.Expr.mvarId! mvar) let y ← tryFinally (Lean.Meta.liftMkBindingM (Lean.MetavarContext.revert toRevertNew mvarId preserveOrder)) (Lean.Meta.setMVarKind mvarId Lean.MetavarKind.syntheticOpaque) _do_jp y