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

Equations

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

def Lean.Elab.Do.tryElabForwardApp? (e : Term) (dec : DoElemCont) : DoElabM (Option Expr)

Elaborate e as an application whose last argument is a do← body, performing the effect forwarding. Returns none if e doesn't have that shape.

Strategy: build headApp ?forwarded with a fresh metavariable in the body slot and elaborate it. Lean's elaborator handles named args, defaults, and dot notation. We then check the wrapper's shape against the probe; on success, the lifted body is assigned into ?forwarded and the probe expression itself is the result.

Equations

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