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

fix: cache typos

Browse source
This commit is contained in:
Sebastian Ullrich 2023-10-10 09:32:47 +02:00 • committed by Leonardo de Moura
parent e3b08060d0
commit 6d0a3287e0
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/ExprDefEq.lean
View file

@ -1802,7 +1802,7 @@ private def getDefEqCacheKind (t s : Expr) : MetaM DefEqCacheKind := do
else match (← getConfig).transparency with
| .default => return .permDefault
| .all => return .permAll
| .reducible => return .permDefault
| .reducible => return .permReducible
| .instances => return .permInst
/--
@ -1824,7 +1824,7 @@ private def getCachedResult (keyInfo : DefEqCacheKeyInfo) : MetaM LBool := do
| .permDefault => cache.defEqDefault
| .permAll => cache.defEqAll
| .permInst => cache.defEqInstances
| .permReducible => cache.defEqInstances
| .permReducible => cache.defEqReducible
match cache.find? keyInfo.key with
| some val => return val.toLBool
| none => return .undef