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

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

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

                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

                  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

                    Similar to traverseLambda and traverseForall but with let binders.

                    Equations
                    Instances For

                      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