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/Basic.lean

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

@ -221,8 +221,8 @@ structure Cache where
synthInstance : SynthInstanceCache := {}
whnfDefault : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
whnfAll : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
defEqTrans : DefEqCache := {} -- transient cache for terms containing mvars and nonstardard configuration options, it is frequently reset.
defEqPerm : DefEqCache := {} -- permanent cache for terms not containing mvars and `TransparencyMode.reducible`
defEqTrans : DefEqCache := {} -- transient cache for terms containing mvars or using nonstandard configuration options, it is frequently reset.
defEqPerm : DefEqCache := {} -- permanent cache for terms not containing mvars and using standard configuration options
deriving Inhabited
/--