We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e551a36 commit b396bdfCopy full SHA for b396bdf
src/Lean/Meta/WHNF.lean
@@ -798,10 +798,12 @@ mutual
798
else
799
unfoldDefault ()
800
| .const declName lvls => do
801
+ let some cinfo ← getUnfoldableConstNoEx? declName | pure none
802
+ -- check smart unfolding only after `getUnfoldableConstNoEx?` because `Environment.contains`
803
+ -- misses are more costly
804
if smartUnfolding.get (← getOptions) && (← getEnv).contains (mkSmartUnfoldingNameFor declName) then
805
return none
806
- let some cinfo ← getUnfoldableConstNoEx? declName | pure none
807
unless cinfo.hasValue do return none
808
deltaDefinition cinfo lvls
809
(fun _ => pure none)
0 commit comments