Documentation

Lean.Compiler.CSimpAttr

structure Lean.Compiler.CSimp.Entry:

Type

fromDeclName : Lean.Name
toDeclName : Lean.Name
thmName : Lean.Name

instance Lean.Compiler.CSimp.instInhabitedEntry:

Inhabited Lean.Compiler.CSimp.Entry

Equations

Lean.Compiler.CSimp.instInhabitedEntry = { default := { fromDeclName := default, toDeclName := default, thmName := default } }

structure Lean.Compiler.CSimp.State:

Type

map : Lean.SMap Lean.Name Lean.Name
thmNames : Lean.SSet Lean.Name

instance Lean.Compiler.CSimp.instInhabitedState:

Inhabited Lean.Compiler.CSimp.State

Equations

Lean.Compiler.CSimp.instInhabitedState = { default := { map := default, thmNames := default } }

def Lean.Compiler.CSimp.State.switch:

Lean.Compiler.CSimp.State → Lean.Compiler.CSimp.State

Equations

Lean.Compiler.CSimp.State.switch _fun_discr = match _fun_discr with | { map := map, thmNames := thmNames } => { map := Lean.SMap.switch map, thmNames := Lean.SSet.switch thmNames }

opaque Lean.Compiler.CSimp.ext:

Lean.SimpleScopedEnvExtension Lean.Compiler.CSimp.Entry Lean.Compiler.CSimp.State

def Lean.Compiler.CSimp.add (declName : Lean.Name) (kind : Lean.AttributeKind) :

Lean.CoreM Unit

Equations

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

@[export lean_csimp_replace_constants]

def Lean.Compiler.CSimp.replaceConstants (env : Lean.Environment) (e : Lean.Expr) :

Equations

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

def Lean.Compiler.hasCSimpAttribute (env : Lean.Environment) (declName : Lean.Name) :

Equations

Lean.Compiler.hasCSimpAttribute env declName = Lean.SSet.contains (Lean.ScopedEnvExtension.getState Lean.Compiler.CSimp.ext env).thmNames declName