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 } }

constant Lean.closedTermCacheExt :

Lean.EnvExtension Lean.ClosedTermCache

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

Lean.Environment

Equations

Lean.cacheClosedTermName env e n = Lean.EnvExtension.modifyState Lean.closedTermCacheExt env fun s => { map := Std.PersistentHashMap.insert s.map e n, constNames := Lean.NameSet.insert s.constNames n }

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