structure Lean.ClosedTermCache : Type

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

instance Lean.instInhabitedClosedTermCache : Inhabited Lean.ClosedTermCache

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

@[export lean_get_closed_term_name]

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

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