structure Lean.Elab.Do.MonadInfo : Type

• m : Expr

  The inferred type of the monad of type Type u → Type v.

• u : Level

  The u in m : Type u → Type v.

• v : Level

  The v in m : Type u → Type v.

• cachedPUnit : Expr

  The cached PUnit expression.

• cachedPUnitUnit : Expr

  The cached PUnit.unit expression.

def Lean.Elab.Do.ContInfoRef : Type

Equations

• Lean.Elab.Do.ContInfoRef = Lean.Elab.Do.ContInfoRefPointed✝.type

instance Lean.Elab.Do.instNonemptyContInfoRef : Nonempty ContInfoRef

def Lean.Elab.Do.DoOpsRef : Type

Equations

• Lean.Elab.Do.DoOpsRef = Lean.Elab.Do.DoOpsRefPointed✝.type

instance Lean.Elab.Do.instNonemptyDoOpsRef : Nonempty DoOpsRef

inductive Lean.Elab.Do.CodeLiveness : Type

Whether a code block is alive or dead.

• deadSyntactically : CodeLiveness

  We inferred the code is syntactically dead and don't need to elaborate it at all.

• deadSemantically : CodeLiveness

  We inferred the code is semantically dead, but we need to elaborate it to produce a program.

• alive : CodeLiveness

  The code is alive. (Or it is dead, but we failed to prove it so.)

@[implicit_reducible]

instance Lean.Elab.Do.instToStringCodeLiveness : ToString CodeLiveness

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Lean.Elab.Do.instToMessageDataCodeLiveness : ToMessageData CodeLiveness

Equations

• Lean.Elab.Do.instToMessageDataCodeLiveness = { toMessageData := fun (l : Lean.Elab.Do.CodeLiveness) => (Lean.MessageData.ofFormat ∘ Std.format) (toString l) }

def Lean.Elab.Do.CodeLiveness.lub (a b : CodeLiveness) : CodeLiveness

The least upper bound of two code livenesses.

Equations

• Lean.Elab.Do.CodeLiveness.alive.lub b = Lean.Elab.Do.CodeLiveness.alive
• a.lub Lean.Elab.Do.CodeLiveness.alive = Lean.Elab.Do.CodeLiveness.alive
• Lean.Elab.Do.CodeLiveness.deadSyntactically.lub b = b
• a.lub Lean.Elab.Do.CodeLiveness.deadSyntactically = a
• a.lub b = a

structure Lean.Elab.Do.MutVar : Type

A mutable variable declared by let mut in a do block.

• ident : Ident

  The identifier of the let mut declaration.

• baseId : FVarId

  The FVarId of the initial binding produced by let mut.

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedMutVar : Inhabited MutVar

Equations

• Lean.Elab.Do.instInhabitedMutVar = { default := Lean.Elab.Do.instInhabitedMutVar.default }

def Lean.Elab.Do.MutVar.getId (mutVar : MutVar) : Name

The raw Name of a mut variable, as found in the local context.

Equations

• mutVar.getId = Lean.TSyntax.getId mutVar.ident

def Lean.Elab.Do.MutVar.mkAliasInfo (mutVar : MutVar) (id : FVarId) : FVarAliasInfo

Build an FVarAliasInfo recording that the reassignment binding id aliases the original let mut binding represented by mutVar.

Equations

• mutVar.mkAliasInfo id = { userName := mutVar.getId, id := id, baseId := mutVar.baseId }

@[implicit_reducible]

instance Lean.Elab.Do.instToMessageDataMutVar : ToMessageData MutVar

Equations

• One or more equations did not get rendered due to their size.

structure Lean.Elab.Do.Context : Type

• monadInfo : MonadInfo

  Inferred and cached information about the monad.

• mutVars : Array MutVar

  The mutable variables in declaration order. Kept in sync with mutVarDefs; insertions go through declareMutVar / declareMutVars only.

• mutVarDefs : Std.HashMap Name MutVar

  Maps mutable variable names to their MutVar record. Kept in sync with mutVars.

• doBlockResultType : Expr

  The expected type of the current do block. This can be different from ReturnCont.resultType in for loop do blocks, for example.

• contInfo : ContInfoRef

  Information about return, break and continue continuations.

• deadCode : CodeLiveness

  Whether the current do element is dead code. elabDoElem will emit a warning if not .alive.

• ops : DoOpsRef

  Pluggable builders for pure and bind applications.

@[reducible, inline]

abbrev Lean.Elab.Do.DoElabM (α : Type) : Type

Equations

• Lean.Elab.Do.DoElabM = ReaderT Lean.Elab.Do.Context Lean.Elab.TermElabM

structure Lean.Elab.Do.DoOps : Type

Pluggable builders for the pure / bind applications emitted by the do elaborator.

• mkPureApp (α e : Expr) : DoElabM Expr

  Build pure (α:=α) e : m α.

• mkBindApp (α β e k : Expr) : DoElabM Expr

  Build bind (α:=α) (β:=β) e k : m β.

• isPureApp? : Expr → Option Expr

  If e is syntactically a pure … application, return the pure value; otherwise none. Used by DoElemCont.mkBindUnlessPure to contract e >>= pure to e and pure e >>= k to let x := e; k x.

• splitMonadApp? : Expr → TermElabM (Option (MonadInfo × Expr))

  Match a monad application m α, returning MonadInfo for m and α.

• mkMonadApp : Expr → DoElabM Expr

  Construct m α from α.

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedDoOps : Inhabited DoOps

Equations

• Lean.Elab.Do.instInhabitedDoOps = { default := Lean.Elab.Do.instInhabitedDoOps.default }

unsafe def Lean.Elab.Do.DoOps.toDoOpsRefImpl (o : DoOps) : DoOpsRef

Equations

• o.toDoOpsRefImpl = unsafeCast o

@[implemented_by Lean.Elab.Do.DoOps.toDoOpsRefImpl]

opaque Lean.Elab.Do.DoOps.toDoOpsRef (o : DoOps) : DoOpsRef

unsafe def Lean.Elab.Do.DoOpsRef.toDoOpsImpl (r : DoOpsRef) : DoOps

Equations

• r.toDoOpsImpl = unsafeCast r

@[implemented_by Lean.Elab.Do.DoOpsRef.toDoOpsImpl]

opaque Lean.Elab.Do.DoOpsRef.toDoOps (r : DoOpsRef) : DoOps

inductive Lean.Elab.Do.DoElemContKind : Type

Whether the continuation of a do element is duplicable. Saying nonDuplicable is always safe; duplicable allows for more optimizations.

• nonDuplicable : DoElemContKind
• duplicable : DoElemContKind

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedDoElemContKind : Inhabited DoElemContKind

Equations

• Lean.Elab.Do.instInhabitedDoElemContKind = { default := Lean.Elab.Do.instInhabitedDoElemContKind.default }

structure Lean.Elab.Do.DoElemCont : Type

Elaboration of a do block do $e; $rest, results in a call elabTerm `(do $e; $rest) = elabDoElem e dec, where elabDoElem e · is the elaborator for do element e, and dec is the DoElemCont describing the elaboration of the rest of the block rest.

If the semantics of e resumes its continuation rest, its elaborator must bind its result to resultName, ensure that it has type resultType and then elaborate rest using dec.

Clearly, for term elements e : m α, the result has type α. More subtly, for binding elements let x := e or let x ← e, the result has type PUnit and is unrelated to the type of the bound variable x.

Examples:

• return drops the continuation; return x; pure () elaborates to pure x.
• let x ← e; rest x elaborates to e >>= fun x => rest x.
• let x := 3; let y ← (let x ← e); rest x elaborates to let x := 3; e >>= fun x_1 => let y := (); rest x, which is immediately zeta-reduced to let x := 3; e >>= fun x_1 => rest x.
• one; two elaborates to one >>= fun (_ : PUnit) => two; it is an error if one does not have type PUnit.

• resultName : Name

  The name of the monadic result variable.

• resultType : Expr

  The type of the monadic result.

• k : DoElabM Expr

  The continuation to elaborate the rest of the block. It assumes that the result of the do block is bound to resultName with the correct type (that is, resultType, potentially refined by a dependent match).

• kind : DoElemContKind

  Whether we are OK with generating the code of the continuation multiple times, e.g. in different branches of a match or if.

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedDoElemCont : Inhabited DoElemCont

Equations

• Lean.Elab.Do.instInhabitedDoElemCont = { default := Lean.Elab.Do.instInhabitedDoElemCont.default }

@[reducible, inline]

abbrev Lean.Elab.Do.DoElab : Type

The type of elaborators for do block elements.

It is elabTerm `(do $e; $rest) = elabDoElem e dec, where elabDoElem e · is the elaborator for do element e, and dec is the DoElemCont describing the elaboration of the rest of the block rest.

Equations

• Lean.Elab.Do.DoElab = (Lean.DoElem → Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr)

structure Lean.Elab.Do.ReturnCont : Type

• resultType : Expr
• k : Expr → DoElabM Expr

  The elaborator constructing a jump site to the return continuation, given some return value. The type of this return value determines the type of the jump expression; this could very well be different than the resultType in case an intervening match has refined resultType. So k must not hardcode the type resultType into its definition; rather it should infer the type of the return value argument.

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedReturnCont : Inhabited ReturnCont

Equations

• Lean.Elab.Do.instInhabitedReturnCont = { default := Lean.Elab.Do.instInhabitedReturnCont.default }

structure Lean.Elab.Do.ContInfo : Type

Information about a success, return, break or continue continuation that will be filled in after the code using it has been elaborated.

• returnCont : ReturnCont
• breakCont : Option (DoElabM Expr)
• continueCont : Option (DoElabM Expr)

@[implicit_reducible]

instance Lean.Elab.Do.instInhabitedContInfo : Inhabited ContInfo

Equations

• Lean.Elab.Do.instInhabitedContInfo = { default := Lean.Elab.Do.instInhabitedContInfo.default }

unsafe def Lean.Elab.Do.ContInfo.toContInfoRefImpl (m : ContInfo) : ContInfoRef

Equations

• m.toContInfoRefImpl = unsafeCast m

@[implemented_by Lean.Elab.Do.ContInfo.toContInfoRefImpl]

opaque Lean.Elab.Do.ContInfo.toContInfoRef (m : ContInfo) : ContInfoRef

unsafe def Lean.Elab.Do.ContInfoRef.toContInfoImpl (m : ContInfoRef) : ContInfo

Equations

• m.toContInfoImpl = unsafeCast m

@[implemented_by Lean.Elab.Do.ContInfoRef.toContInfoImpl]

opaque Lean.Elab.Do.ContInfoRef.toContInfo (m : ContInfoRef) : ContInfo

def Lean.Elab.Do.mkMonadApp (resultType : Expr) : DoElabM Expr

Constructs m α from α.

Equations

• Lean.Elab.Do.mkMonadApp resultType = do let __do_lift ← read __do_lift.ops.toDoOps.mkMonadApp resultType

def Lean.Elab.Do.mkPUnit : DoElabM Expr

The cached PUnit expression.

Equations

• Lean.Elab.Do.mkPUnit = do let __do_lift ← read pure __do_lift.monadInfo.cachedPUnit

def Lean.Elab.Do.mkPUnitUnit : DoElabM Expr

The cached PUnit.unit expression.

Equations

• Lean.Elab.Do.mkPUnitUnit = do let __do_lift ← read pure __do_lift.monadInfo.cachedPUnitUnit

def Lean.Elab.Do.mkPureApp (α e : Expr) : DoElabM Expr

The expression pure (α:=α) e.

Equations

• Lean.Elab.Do.mkPureApp α e = do let __do_lift ← read __do_lift.ops.toDoOps.mkPureApp α e

def Lean.Elab.Do.DoElemCont.mkPure (resultType : Expr) : TermElabM DoElemCont

Create a DoElemCont returning the result using pure.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.ReturnCont.mkPure (resultType : Expr) : TermElabM ReturnCont

Create a ReturnCont returning the result using pure.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.mkBindApp (α β e k : Expr) : DoElabM Expr

The expression Bind.bind (α:=α) (β:=β) e k.

Equations

• Lean.Elab.Do.mkBindApp α β e k = do let __do_lift ← read __do_lift.ops.toDoOps.mkBindApp α β e k

def Lean.Elab.Do.DoOps.default : DoOps

DoOps emitting Pure.pure / Bind.bind.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.declareMutVar {α : Type} (x : Ident) (k : DoElabM α) : DoElabM α

Register the given name as that of a mut variable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.declareMutVars {α : Type} (xs : Array Ident) (k : DoElabM α) : DoElabM α

Register the given names as that of mut variables.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.declareMutVar? {α : Type} (mutTk? : Option Syntax) (x : Ident) (k : DoElabM α) : DoElabM α

Register the given name as that of a mut variable if the syntax token mut is present.

Equations

• Lean.Elab.Do.declareMutVar? mutTk? x k = if mutTk?.isSome = true then Lean.Elab.Do.declareMutVar x k else k

def Lean.Elab.Do.declareMutVars? {α : Type} (mutTk? : Option Syntax) (xs : Array Ident) (k : DoElabM α) : DoElabM α

Register the given names as that of mut variables if the syntax token mut is present.

Equations

• Lean.Elab.Do.declareMutVars? mutTk? xs k = if mutTk?.isSome = true then Lean.Elab.Do.declareMutVars xs k else k

def Lean.Elab.Do.findMutVar? (n : Name) : DoElabM (Option MutVar)

Look up a declared mut variable by its raw Name.

Equations

• Lean.Elab.Do.findMutVar? n = do let __do_lift ← read pure __do_lift.mutVarDefs[n]?

def Lean.Elab.Do.throwUnlessMutVarDeclared (x : Ident) : DoElabM Unit

Throw an error if the given name is not a declared mut variable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.throwUnlessMutVarsDeclared (xs : Array Ident) : DoElabM Unit

Throw an error if the given names are not declared mut variables.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.checkMutVarsForShadowingOne (x : Ident) : DoElabM Unit

Throw an error if a declaration of the given name would shadow a mut variable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.checkMutVarsForShadowing (xs : Array Ident) : DoElabM Unit

Throw an error if a declaration of the given name would shadow a mut variable.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.mkFreshResultType (userName : Name := `α) (kind : MetavarKind := MetavarKind.natural) : DoElabM Expr

Create a fresh α that would fit in m α.

Equations

• Lean.Elab.Do.mkFreshResultType userName kind = do let __do_lift ← read liftM (Lean.Meta.mkFreshExprMVar (some (Lean.mkSort (Lean.mkLevelSucc __do_lift.monadInfo.u))) kind userName)

@[inline]

def Lean.Elab.Do.controlAtTermElabM {α : Type} (k : ({β : Type} → DoElabM β → TermElabM β) → TermElabM α) : DoElabM α

Like controlAt TermElabM, but it maintains the state using the DoElabM's ref cell instead of returning it in the TermElabM result. This makes it possible to run multiple DoElabM computations in a row.

Equations

• Lean.Elab.Do.controlAtTermElabM k ctx = k fun {β : Type} (x : Lean.Elab.Do.DoElabM β) => x ctx

@[inline]

def Lean.Elab.Do.mapTermElabM (f : {α : Type} → TermElabM α → TermElabM α) {α : Type} (k : DoElabM α) : DoElabM α

Equations

• Lean.Elab.Do.mapTermElabM f k = Lean.Elab.Do.controlAtTermElabM fun (runInBase : {β : Type} → Lean.Elab.Do.DoElabM β → Lean.Elab.TermElabM β) => f (runInBase k)

@[inline]

def Lean.Elab.Do.map1TermElabM {β : Sort u_1} (f : {α : Type} → (β → TermElabM α) → TermElabM α) {α : Type} (k : β → DoElabM α) : DoElabM α

Equations

• Lean.Elab.Do.map1TermElabM f k = Lean.Elab.Do.controlAtTermElabM fun (runInBase : {β : Type} → Lean.Elab.Do.DoElabM β → Lean.Elab.TermElabM β) => f fun (b : β) => runInBase (k b)

def Lean.Elab.Do.withDeadCode {α : Type} (deadCode : CodeLiveness) (k : DoElabM α) : DoElabM α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.getReassignedMutVars (rootCtx : LocalContext) (mutVars : Std.HashSet Name) (childCtxs : Array LocalContext) : Std.HashSet Name

The subset of mutVars that were reassigned in any of the childCtxs relative to the given rootCtx.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.withLCtxKeepingMutVarDefs {α : Type} (oldLCtx : LocalContext) (oldCtx : Context) (resultName : Name) (k : DoElabM α) : DoElabM α

Restores the local context to oldCtx and adds the new reaching definitions of the mut vars and result. Then resume the continuation k with the mutVars restored to the given oldMutVars.

This function is useful to de-nest

let mut x := 0
let y := 3
let z ← do
  let mut y ← e
  x := y + 1
  pure y
let y := y + 3
pure (x + y + z)

into

let mut x := 0
let y := 3
let mut y† ← e
x := y† + 1
let z ← pure y†
let y := y + 3
pure (x + y + z)

Note that the continuation of the let z ← ... bind, roughly k := .cont `z _ `(let y := y + 3; pure (x + y + z)), needs to be elaborated in a local context that contains the reassignment of x, but not the shadowing mut var definition of y.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.mkMonadicResultTypeMismatchError (contType elementType : Expr) : MessageData

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.DoElemCont.ensureHasTypeAt (dec : DoElemCont) (ref : Syntax) (elementType : Expr) : DoElabM DoElemCont

Given a continuation dec, a reference ref, and an element result type elementType, returns a continuation derived from dec with result type elementType. If dec already has result type elementType, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result. The error is reported at ref.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.DoElemCont.ensureUnitAt (dec : DoElemCont) (ref : Syntax) : DoElabM DoElemCont

Given a continuation dec and a reference ref, returns a continuation derived from dec with result type PUnit. If dec already has result type PUnit, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result. The error is reported at ref.

Equations

• dec.ensureUnitAt ref = do let __do_lift ← Lean.Elab.Do.mkPUnit dec.ensureHasTypeAt ref __do_lift

def Lean.Elab.Do.DoElemCont.ensureUnit (dec : DoElemCont) : DoElabM DoElemCont

Given a continuation dec, returns a continuation derived from dec with result type PUnit. If dec already has result type PUnit, simply returns dec. Otherwise, an error is logged and a new continuation is returned that calls dec with sorry as a result.

Equations

• dec.ensureUnit = do let __do_lift ← Lean.getRef dec.ensureUnitAt __do_lift

def Lean.Elab.Do.DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr

Return $e >>= fun ($dec.resultName : $dec.resultType) => $(← dec.k), cancelling the bind if $(← dec.k) is pure $dec.resultName or e is some pure computation.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.DoElemCont.continueWithUnit (dec : DoElemCont) : DoElabM Expr

Return let $k.resultName : PUnit := PUnit.unit; $(← k.k), ensuring that the result type of k.k is PUnit and then immediately zeta-reduce the let.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.DoElemCont.elabAsSyntacticallyDeadCode (dec : DoElemCont) : DoElabM Unit

Elaborate the DoElemCont with the deadCode flag set to deadSyntactically to emit warnings.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.DoElemCont.withDeadCodeFromInfo (dec : DoElemCont) (info : ControlInfo) : DoElemCont

Wrap dec.k so it elaborates as dead iff info.noFallthrough.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.bindMutVarsFromTuple (vars : List Name) (tupleVar : FVarId) (k : DoElabM Expr) : DoElabM Expr

Given a list of mut vars vars and an FVar tupleVar binding a tuple, bind the mut vars to the fields of the tuple and call k in the resulting local context.

Equations

• Lean.Elab.Do.bindMutVarsFromTuple vars tupleVar k = do let __do_lift ← liftM tupleVar.getType Lean.Elab.Do.bindMutVarsFromTuple.go✝ k vars tupleVar __do_lift #[]

structure Lean.Elab.Do.SavedState : Type

Backtrackable state for the TermElabM monad.

• term : Term.SavedState

instance Lean.Elab.Do.instNonemptySavedState : Nonempty SavedState

def Lean.Elab.Do.SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : DoElabM Unit

Equations

• s.restore restoreInfo = liftM (s.term.restore restoreInfo)

def Lean.Elab.Do.DoElabM.saveState : DoElabM SavedState

Equations

• Lean.Elab.Do.DoElabM.saveState = do let __do_lift ← liftM Lean.Elab.Term.saveState pure { term := __do_lift }

@[implicit_reducible]

instance Lean.Elab.Do.instMonadBacktrackSavedStateDoElabM : MonadBacktrack SavedState DoElabM

Equations

• Lean.Elab.Do.instMonadBacktrackSavedStateDoElabM = { saveState := Lean.Elab.Do.DoElabM.saveState, restoreState := fun (b : Lean.Elab.Do.SavedState) => b.restore }

def Lean.Elab.Do.observingPostpone {α : Type} (x : DoElabM α) : DoElabM (Option α)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.doElabToSyntaxWithExpectedType {α : Type} (hint : MessageData) (doElab : Option Expr → DoElabM Expr) (k : Term → DoElabM α) (ref : Syntax := Syntax.missing) : DoElabM α

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.doElabToSyntax {α : Type} (hint : MessageData) (doElab : DoElabM Expr) (k : Term → DoElabM α) (ref : Syntax := Syntax.missing) : DoElabM α

Equations

• Lean.Elab.Do.doElabToSyntax hint doElab k ref = Lean.Elab.Do.doElabToSyntaxWithExpectedType hint (fun (_ty? : Option Lean.Expr) => doElab) k ref

def Lean.Elab.Do.DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : ControlInfo) (caller : DoElemCont → DoElabM Expr) : DoElabM Expr

Call caller with a duplicable proxy of dec. When the proxy is elaborated more than once, a join point is introduced so that dec is only elaborated once to fill in the RHS of this join point.

This is useful for control-flow constructs like if and match, where multiple tail-called branches share the continuation.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.getReturnCont : DoElabM ReturnCont

Equations

• Lean.Elab.Do.getReturnCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.returnCont

def Lean.Elab.Do.getBreakCont : DoElabM (Option (DoElabM Expr))

Equations

• Lean.Elab.Do.getBreakCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.breakCont

def Lean.Elab.Do.getContinueCont : DoElabM (Option (DoElabM Expr))

Equations

• Lean.Elab.Do.getContinueCont = do let __do_lift ← read pure __do_lift.contInfo.toContInfo.continueCont

@[inline]

def Lean.Elab.Do.withDoBlockResultType {α : Type} (doBlockResultType : Expr) (k : DoElabM α) : DoElabM α

Set the new do block result type for the scope of the continuation k.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.enterLoopBody {α : Type} (breakCont continueCont : DoElabM Expr) (returnCont : ReturnCont) (body : DoElabM α) : DoElabM α

Prepare the context for elaborating the body of a loop. This includes setting the return continuation, break continuation, continue continuation, as well as the changed result type of the do block in the loop body.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.withoutControl (k : DoElabM Expr) : DoElabM Expr

Prepare the context for elaborating the body of a do block that does not support mut vars, break, continue or return.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.enterFinally (resultType : Expr) (k : DoElabM Expr) : DoElabM Expr

Prepare the context for elaborating the body of a finally block. There is no support for mut vars, break, continue or return in a finally block.

Equations

• Lean.Elab.Do.enterFinally resultType k = Lean.Elab.Do.withoutControl (Lean.Elab.Do.withDoBlockResultType resultType k)

def Lean.Elab.Do.mkContext (expectedType? : Option Expr) (ops : DoOps := DoOps.default) : TermElabM Context

Create the Context for do elaboration from the given expected type of a do block.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.expandNestedActions {kind : SyntaxNodeKinds} (stx : TSyntax kind) : DoElabM (Array DoElem × TSyntax kind)

Equations

• One or more equations did not get rendered due to their size.

unsafe def Lean.Elab.Do.mkDoElemElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute DoElab)

Equations

• Lean.Elab.Do.mkDoElemElabAttributeUnsafe ref = Lean.Elab.mkElabAttribute Lean.Elab.Do.DoElab `builtin_doElem_elab `doElem_elab `Lean.Parser.Term.doElem `Lean.Elab.Do.DoElab "do element" ref

@[implemented_by Lean.Elab.Do.mkDoElemElabAttributeUnsafe]

opaque Lean.Elab.Do.mkDoElemElabAttribute (ref : Name) : IO (KeyedDeclsAttribute DoElab)

opaque Lean.Elab.Do.doElemElabAttribute : KeyedDeclsAttribute DoElab

Registers a do element elaborator for the given syntax node kind.

A do element elaborator should have type DoElab (which is Lean.Syntax → DoElemCont → DoElabM Expr), i.e. should take syntax of the given syntax node kind and a DoElemCont as parameters and produce an expression.

When elaborating a do block do e; rest, the elaborator for e is invoked with the syntax of e and the DoElemCont representing rest.

The elab_rules and elab commands should usually be preferred over using this attribute directly.

partial def Lean.Elab.Do.elabDoElem (stx : DoElem) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

partial def Lean.Elab.Do.elabDoElems1 (doElems : Array DoElem) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

partial def Lean.Elab.Do.elabDoSeq (doSeq : DoSeq) (cont : DoElemCont) (catchExPostpone : Bool := true) : DoElabM Expr

def Lean.Elab.Do.elabNestedAction : Term.TermElab

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.elabDoWith (ops : DoOps) (doSeq : DoSeq) (expectedType? : Option Expr) : TermElabM Expr

Elaborate doSeq using ops for pure/bind construction.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Do.elabDo : Term.TermElab

Equations

• One or more equations did not get rendered due to their size.