structure Lean.Compiler.CSimp.Entry : Type

• fromDeclName : Name
• toDeclName : Name
• thmName : Name

instance Lean.Compiler.CSimp.instInhabitedEntry : Inhabited Entry

def Lean.Compiler.CSimp.instInhabitedEntry.default : Entry

structure Lean.Compiler.CSimp.State : Type

• map : SMap Name Name
• thmNames : SSet Name

def Lean.Compiler.CSimp.instInhabitedState.default : State

instance Lean.Compiler.CSimp.instInhabitedState : Inhabited State

def Lean.Compiler.CSimp.State.switch : State → State

opaque Lean.Compiler.CSimp.ext : SimpleScopedEnvExtension Entry State

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

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

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