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 7fa7c46Copy full SHA for 7fa7c46
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 smart unfoldings have a
803
+ -- significant chance of not existing and `Environment.contains` 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