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

fix: caching condition

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-04 16:14:26 -08:00
parent e3b8013c4e
commit f570d2a1c3
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/Lean/Meta/SynthInstance.lean
View file

@ -530,10 +530,10 @@ usingTransparency TransparencyMode.reducible $ do
(pure (some result)))
(pure none)
};
if type.hasMVar then do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s };
if type.hasMVar then
pure result
else
else do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s };
pure result
/--