max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unnecessary partial

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-30 15:47:31 -07:00
parent e9e75af834
commit 2c152dae7d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/WHNF.lean
View file

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