structure Lean.Elab.Do.ForwardArg : Type

A body that effect-forwards into the enclosing do block via a do← marker, captured from syntax of the form do← body or fun b₁ … bₖ => do← body. binders is empty in the bare form.

• binders : Array (TSyntax `Lean.Parser.Term.funBinder)
• body : DoSeq

def Lean.Elab.Do.Forward.matchApp? (e : Term) : Option (Term × ForwardArg)

If e is a function application whose last argument effect-forwards into the enclosing do block (its body bears a do← marker, possibly under fun binders), return the application head sans the forwarding argument together with the ForwardArg description.

Equations

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