structure Lean.ClosedTermCache : Type

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

def Lean.instInhabitedClosedTermCache.default : ClosedTermCache

Equations

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

@[implicit_reducible]

instance Lean.instInhabitedClosedTermCache : Inhabited ClosedTermCache

Equations

• Lean.instInhabitedClosedTermCache = { default := Lean.instInhabitedClosedTermCache.default }

opaque Lean.closedTermCacheExt : EnvExtension ClosedTermCache

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

Equations

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

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

Equations

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

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

Equations

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