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

chore: update comments at src/Lean/Meta/ExprDefEq.lean

Browse source 
Co-authored-by: Timo <timorcb@gmail.com>
This commit is contained in:
Leonardo de Moura 2023-10-11 15:51:11 -07:00 • committed by Leonardo de Moura
parent 3bc18797b0
commit 29198371d9
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

@ -1793,8 +1793,8 @@ private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
isDefEqOnFailure t s
inductive DefEqCacheKind where
| transient -- problem has mvars or is using nonstardard configuration, we should use transient cache
| permanent -- problem does not have mvars and we are using stardard config, we can use one persistent cache.
| transient -- problem has mvars or is using nonstandard configuration, we should use transient cache
| permanent -- problem does not have mvars and we are using standard config, we can use one persistent cache.
private def getDefEqCacheKind (t s : Expr) : MetaM DefEqCacheKind := do
if t.hasMVar || s.hasMVar || (← read).canUnfold?.isSome then