From b110d800e9bb698b1bf5ab501ef28b90a1afa522 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Thu, 9 Jun 2022 20:03:30 -0400
Subject: [PATCH] fix: add ExprTraversal to Meta

---
 src/Lean/Meta.lean           | 1 +
 tests/lean/run/ExprLens.lean | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index e2cbdbf943..4d7509d010 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -41,3 +41,4 @@ import Lean.Meta.CongrTheorems
 import Lean.Meta.Eqns
 import Lean.Meta.CasesOn
 import Lean.Meta.ExprLens
+import Lean.Meta.ExprTraverse
diff --git a/tests/lean/run/ExprLens.lean b/tests/lean/run/ExprLens.lean
index 9b7f33b198..b7ade10c25 100644
--- a/tests/lean/run/ExprLens.lean
+++ b/tests/lean/run/ExprLens.lean
@@ -46,7 +46,7 @@ def testTraversal
       dbg_trace s!"{p}, {ppt}\n"
     throwError "expected size: {expectedLen}\nactual size: {subexprs.size}"
   for (p, s) in subexprs do
-    let e3 ← viewSubexpr (fun fvars t => do
+    let _ ← viewSubexpr (fun fvars t => do
       let t := Expr.abstract t fvars
       let de ← liftM $ isDefEq t s
       if not de then