Tools for extracting Exprs from MessageData nodes

This file provides for (ppCtx, e) in msg.exprs do notation, which iterates through the expressions e in a msg : MessageData. The surrounding monad must support BaseIO to handle .ofLazy MessageData nodes. e may be interpreted in a MetaM context using ppCtx.runMetaM e.

Some helpers are provided implemented in terms of this.

def Lean.MessageData.forExprsIn {m : Type → Type u} [Monad m] [MonadLiftT BaseIO m] {σ : Type} (msg : MessageData) (s : σ) (f : PPContext × Expr → σ → m (ForInStep σ)) : m σ

Iterate over all the expressions in a MessageData. Used to implement for (ppCtx, e) in msg.exprs do notation, which should be preferred over using this declaration directly.

structure Lean.MessageData.Exprs : Type

A wrapper structure for MessageData to enable for (ppCtx, e) in msg.exprs do notation.

• msg : MessageData

  The MessageData whose expressions will be iterated over.

def Lean.MessageData.exprs (msg : MessageData) : MessageData.Exprs

for (ppCtx, e) in msg.exprs do iterates through the expressions in MessageData together with their ppCtx : PPContext. The ppCtx can be used to interpret the expression in a valid MetaM context via ppCtx.runMetaM.

The monad must support BaseIO in order to interpret .ofLazy nodes in MessageData.

Expressions without a valid ppCtx are skipped.

@[implicit_reducible]

instance Lean.MessageData.instForInExprsProdPPContextExpr {m : Type → Type u} [Monad m] [MonadLiftT BaseIO m] : ForIn m MessageData.Exprs (PPContext × Expr)

def Lean.MessageData.firstExpr? {α : Type} (msg : MessageData) (f : Expr → MetaM (Option α)) : IO (Option α)

Find the expression in a message on which f does not return none.

def Lean.MessageData.getExprs {m : Type → Type u} [Monad m] [MonadLiftT BaseIO m] (msg : MessageData) : m (Array Expr)

Get all the expressions in a message, in order.

If you need the context of the expressions, prefer iterating over the expressions via for (ppCtx, e) in msg.exprs do directly.