From b8af36fba09ed866e0541083973a4f870a32fe0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Oct 2023 15:51:40 -0700 Subject: [PATCH] chore: update comments at src/Lean/Meta/Basic.lean Co-authored-by: Timo --- src/Lean/Meta/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index aeecb2b9a1..84a759cfcc 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -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 /--