structure Lean.ClosedTermCache : Type

• map : PHashMap Expr Name
• constNames : NameSet
• revExprs : List Expr

instance Lean.instInhabitedClosedTermCache : Inhabited ClosedTermCache

opaque Lean.closedTermCacheExt : EnvExtension ClosedTermCache

@[export lean_cache_closed_term_name]

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

@[export lean_get_closed_term_name]

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

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