structure Lean.ClosedTermCache : Type

• map : Lean.PHashMap Lean.Expr Lake.Name
• constNames : Lean.NameSet

instance Lean.instInhabitedClosedTermCache : Inhabited Lean.ClosedTermCache

Equations

• Lean.instInhabitedClosedTermCache = { default := { map := default, constNames := default } }

opaque Lean.closedTermCacheExt : Lean.EnvExtension Lean.ClosedTermCache

@[export lean_cache_closed_term_name]

def Lean.cacheClosedTermName (env : Lean.Environment) (e : Lean.Expr) (n : Lake.Name) : Lean.Environment

Equations

• One or more equations did not get rendered due to their size.

@[export lean_get_closed_term_name]

def Lean.getClosedTermName? (env : Lean.Environment) (e : Lean.Expr) : Option Lake.Name

Equations

• Lean.getClosedTermName? env e = Lean.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.closedTermCacheExt env).map e

def Lean.isClosedTermName (env : Lean.Environment) (n : Lake.Name) : Bool

Equations

• Lean.isClosedTermName env n = Lean.NameSet.contains (Lean.EnvExtension.getState Lean.closedTermCacheExt env).constNames n