def Lean.Elab.Do.expandDoFor : Macro

Equations

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

structure Lean.Elab.Do.ForInApp : Type

The already-elaborated pieces of a forIn application that an annotation's gadget is built from.

• xs : Expr

  The collection being iterated.

• init : Expr

  The initial state tuple.

• body : Expr

  The loop body, a function from the element and the state tuple to a ForInStep.

• σ : Expr

  The type of the state tuple.

• statePat : Term

  The pattern naming the loop's mutable variables in the state tuple.

• erasedMutVars : Array MutVar

  The erased variables among the loop's mutable variables; annotations bind their .out projections over the state tuple.

def Lean.Elab.Do.elabDoFor : DoElab

Equations

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