From 2c152dae7de15a6eb897b1f91e644ff3b07a84d3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jun 2022 15:47:31 -0700 Subject: [PATCH] chore: remove unnecessary `partial` --- src/Lean/Meta/WHNF.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index 873603dd60..bb56f4d6eb 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -398,7 +398,7 @@ private def whnfMatcher (e : Expr) : MetaM Expr := do withTransparency transparency <| withReader (fun ctx => { ctx with canUnfold? := canUnfoldAtMatcher }) do whnf e -partial def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do +def reduceMatcher? (e : Expr) : MetaM ReduceMatcherResult := do match e.getAppFn with | Expr.const declName declLevels _ => let some info ← getMatcherInfo? declName