structure Lean.Elab.Do.ControlStack : Type

• description : Unit → MessageData
• m : DoElabM Expr
• stM : Expr → DoElabM Expr
• runInBase : Expr → DoElabM Expr
• restoreCont : DoElemCont → DoElabM DoElemCont

def Lean.Elab.Do.ControlStack.unStM (m : ControlStack) (stMα : Expr) : DoElabM Expr

def Lean.Elab.Do.ControlStack.base (mi : MonadInfo) : ControlStack

def Lean.Elab.Do.ControlStack.stateT (baseMonadInfo : MonadInfo) (mutVars : Array Name) (σ : Expr) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.optionT (baseMonadInfo : MonadInfo) (optionTWrapper casesOnWrapper : Name) (getCont : DoElabM (DoElabM Expr)) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.exceptT (baseMonadInfo : MonadInfo) (exceptTWrapper casesOnWrapper : Name) (getCont : DoElabM ReturnCont) (ε : Expr) (base : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.earlyReturnT (baseMonadInfo : MonadInfo) (ρ : Expr) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.breakT (baseMonadInfo : MonadInfo) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.continueT (baseMonadInfo : MonadInfo) (m : ControlStack) : ControlStack

def Lean.Elab.Do.ControlStack.mkBreak (base : ControlStack) (hasContinue : Bool) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkContinue (base : ControlStack) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkReturn (base : ControlStack) (r : Expr) : DoElabM Expr

def Lean.Elab.Do.ControlStack.mkPure (base : ControlStack) (resultName : Name) : DoElabM Expr

structure Lean.Elab.Do.ControlLifter : Type

• origCont : DoElemCont
• returnBase? : Option ControlStack
• breakBase? : Option ControlStack
• continueBase? : Option ControlStack
• pureBase : ControlStack
• pureDeadCode : CodeLiveness
• liftedDoBlockResultType : Expr

def Lean.Elab.Do.ControlLifter.ofCont (info : ControlInfo) (dec : DoElemCont) : DoElabM ControlLifter

def Lean.Elab.Do.ControlLifter.lift (l : ControlLifter) (elabElem : DoElemCont → DoElabM Expr) : DoElabM Expr

This function is like MonadControl.liftWith fun runInBase => elabElem (runInBase pure). All continuations should be thought of as wrapped in runInBase, so that their effects are embedded in the terminal stM m (t m) result type. This wrapping will be realized by ControlStack.synthesizeConts, after we know what the transformer stack t looks like. What t looks like depends on whether reassignments, early return, break and continue are used, considering all the use sites of ControlLifter.lift.

def Lean.Elab.Do.ControlLifter.restoreCont (l : ControlLifter) : DoElabM DoElemCont