structure Lean.Compiler.CSimp.Entry : Type

• fromDeclName : Lake.Name
• toDeclName : Lake.Name
• thmName : Lake.Name

Instances For

• Lean.Compiler.CSimp.instInhabitedEntry

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 Lake.Name Lake.Name
• thmNames : Lean.SSet Lake.Name

Instances For

• Lean.Compiler.CSimp.instInhabitedState

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

• x.switch = match x with | { map := map, thmNames := thmNames } => { map := map.switch, thmNames := thmNames.switch }

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

def Lean.Compiler.CSimp.add (declName : Lake.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) : Lean.Expr

Equations

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

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

Equations

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