Documentation

Lean.Compiler.ClosedTermCache

structure Lean.ClosedTermCache:

Type

map : Std.PHashMap Lean.Expr Lean.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 : Lean.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 Lean.Name

Equations

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

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

Equations

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