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.

Equations

• msg.forExprsIn s f = do let __do_lift ← Lean.MessageData.forExprsIn.go✝ f { currNamespace := Lean.Name.anonymous, openDecls := [] } none s msg pure __do_lift.value

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.

Equations

• msg.exprs = { msg := msg }

@[implicit_reducible]

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

Equations

• Lean.MessageData.instForInExprsProdPPContextExpr = { forIn := fun {β : Type} (exprs : Lean.MessageData.Exprs) => exprs.msg.forExprsIn }

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.

Equations

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

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.

Equations

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