Documentation

Lean.Meta.ExprTraverse

Similar to traverseLambda but with an additional pos argument to track position.

Equations
    Instances For
      Equations
        Instances For

          Similar to traverseForall but with an additional pos argument to track position.

          Equations
            Instances For
              Equations
                Instances For

                  Similar to traverseLet but with an additional pos argument to track position.

                  Equations
                    Instances For
                      Equations
                        Instances For
                          def Lean.Meta.traverseChildrenWithPos {M : TypeType u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : SubExpr.PosExprM Expr) (p : SubExpr.Pos) (e : Expr) :

                          Similar to Lean.Meta.traverseChildren except that visit also includes a Pos argument so you can track the subexpression position.

                          Equations
                            Instances For
                              def Lean.Meta.traverseLambda {M : TypeType u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : ExprM Expr) (e : Expr) :

                              Given an expression fun (x₁ : α₁) ... (xₙ : αₙ) => b, will run f on each of the variable types αᵢ and b with the correct MetaM context, replacing each expression with the output of f and creating a new lambda. (that is, correctly instantiating bound variables and repackaging them after)

                              Equations
                                Instances For
                                  def Lean.Meta.traverseForall {M : TypeType u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : ExprM Expr) (e : Expr) :

                                  Given an expression (x₁ : α₁) → ... → (xₙ : αₙ) → b, will run f on each of the variable types αᵢ and b with the correct MetaM context, replacing the expression with the output of f and creating a new forall expression. (that is, correctly instantiating bound variables and repackaging them after)

                                  Equations
                                    Instances For
                                      def Lean.Meta.traverseLet {M : TypeType u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : ExprM Expr) (e : Expr) :

                                      Similar to traverseLambda and traverseForall but with let binders.

                                      Equations
                                        Instances For
                                          def Lean.Meta.traverseChildren {M : TypeType u_1} [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (visit : ExprM Expr) (e : Expr) :

                                          Maps visit on each child of the given expression.

                                          Applications, foralls, lambdas and let binders are bundled (as they are bundled in Expr.traverseApp, traverseForall, ...). So traverseChildren f e where e = `(fn a₁ ... aₙ) will return (← f `(fn)) (← f `(a₁)) ... (← f `(aₙ)) rather than (← f `(fn a₁ ... aₙ₋₁)) (← f `(aₙ))

                                          See also Lean.Core.traverseChildren.

                                          Equations
                                            Instances For