diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index 459c2668e1..08f41d776e 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -41,7 +41,7 @@ partial def visit (fn : Expr → MetaM Bool) (e : Expr) : M Unit := | Expr.forallE _ _ _ _ => visitBinder fn #[] 0 e | Expr.lam _ _ _ _ => visitBinder fn #[] 0 e | Expr.letE _ _ _ _ _ => visitBinder fn #[] 0 e - | Expr.app f a _ => do visit fn f; visit fn a + | Expr.app f a _ => visit fn f; visit fn a | Expr.mdata _ b _ => visit fn b | Expr.proj _ _ b _ => visit fn b | _ => pure ()