sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: whnf

Browse Source
This commit is contained in:
Leonardo de Moura
2026-03-03 09:13:44 -08:00
parent 1f04bf4fd1
commit b3b669cdd1
1 changed files with 2 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
src/Lean/Meta/WHNF.lean
View File

@@ -348,7 +348,7 @@ mutual
unless projInfo.fromClass do return none
-- First check whether `e`s instance is stuck.
if let some major := args[projInfo.numParams]? then
if let some mvarId ← getStuckMVar? major then
if let some mvarId ← getStuckMVar? (← whnf major) then
return mvarId
/-
Then, recurse on the explicit arguments
@@ -366,7 +366,7 @@ mutual
else if let some auxInfo ← getAuxParentProjectionInfo? fName then
unless auxInfo.fromClass do return none
if let some major := args[auxInfo.numParams]? then
if let some mvarId ← getStuckMVar? major then
if let some mvarId ← getStuckMVar? (← whnf major) then
return mvarId
return none
else