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