fix: add ExprTraversal to Meta

This commit is contained in:
E.W.Ayers 2022-06-09 20:03:30 -04:00 committed by Leonardo de Moura
parent 4a70143aaf
commit b110d800e9
2 changed files with 2 additions and 1 deletions

View file

@ -41,3 +41,4 @@ import Lean.Meta.CongrTheorems
import Lean.Meta.Eqns
import Lean.Meta.CasesOn
import Lean.Meta.ExprLens
import Lean.Meta.ExprTraverse

View file

@ -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