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

fix: universe metavariables should not be taken into account at getKeyArgs

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-06 07:50:19 -08:00
parent b105c006a5
commit 8bcaafb28b
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/DiscrTree.lean
View file

@ -370,7 +370,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
match e.getAppFn with
| Expr.lit v _ => return (Key.lit v, #[])
| Expr.const c _ _ =>
if (← getConfig).isDefEqStuckEx && e.hasMVar then
if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
if (← isReducible c) then
/- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
This can happen if the metavariables in `e` are "blocking" smart unfolding.