Documentation

Lean.Meta.ForEachExpr

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

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

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

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

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

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

          Equations
          Instances For
            Equations
            Instances For

              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

                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
                  • One or more equations did not get rendered due to their size.
                  Instances For

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    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
                      • One or more equations did not get rendered due to their size.
                      Instances For