From 3d01327129df2d71749c06d37b6507e2404ea321 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Jan 2021 09:45:26 -0800 Subject: [PATCH] chore: remove unnecessary `do` --- src/Lean/Meta/ForEachExpr.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ()