Documentation

Lean.Meta.ForEachExpr

def Lean.Meta.visitLambda {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (e : Expr) :

Given an expression e = fun (x₁ : α₁) .. (xₙ : αₙ) => b, runs f on each αᵢ and b.

Equations
    Instances For
      def Lean.Meta.visitLambda.visit {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (fvars : Array Expr) :
      Exprm Unit
      Equations
        Instances For
          def Lean.Meta.visitForall {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (e : Expr) :

          Given an expression e = (x₁ : α₁) → .. (xₙ : αₙ) → b, runs f on each αᵢ and b.

          Equations
            Instances For
              def Lean.Meta.visitForall.visit {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (fvars : Array Expr) :
              Exprm Unit
              Equations
                Instances For
                  def Lean.Meta.visitLet {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (e : Expr) :

                  Given a sequence of let binders let (x₁ : α₁ := v₁) ... in b, runs f on each αᵢ, vᵢ and b.

                  Equations
                    Instances For
                      def Lean.Meta.visitLet.visit {m : TypeType u_1} [Monad m] [MonadControlT MetaM m] (f : Exprm Unit) (fvars : Array Expr) :
                      Exprm Unit
                      Equations
                        Instances For
                          def Lean.Meta.forEachExpr' {m : TypeType} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (input : Expr) (fn : Exprm Bool) :

                          Similar to Expr.forEach', but creates free variables whenever going inside of a binder. If the inner function returns false, deeper subexpressions will not be visited.

                          Equations
                            Instances For
                              def Lean.Meta.forEachExpr {m : TypeType} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m] (e : Expr) (f : Exprm Unit) :

                              Similar to Expr.forEach, but creates free variables whenever going inside of a binder.

                              Equations
                                Instances For

                                  Auxiliary method for (temporarily) setting the user facing name of metavariables. Let ?m be a metavariable in isTarget.contains ?m, and ?m does not have a user facing name. Then, we try to find an application f ... ?m in e, and (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for ?m. This method returns all metavariables whose user facing name has been updated.

                                  Equations
                                    Instances For

                                      Remove user facing name for metavariables in toReset. This a low-level method for "undoing" the effect of setMVarUserNamesAt

                                      Equations
                                        Instances For

                                          Similar to mkForallFVars, but tries to infer better binder names when xs contains metavariables. Let ?m be a metavariable in xs s.t. ?m does not have a user facing name. Then, we try to find an application f ... ?m in the other binder typer and type, and (temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for ?m. The "renaming" is temporary.

                                          Equations
                                            Instances For