structure Lean.Compiler.CSimp.Entry : Type

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

@[implicit_reducible]

instance Lean.Compiler.CSimp.instInhabitedEntry : Inhabited Entry

Equations

• Lean.Compiler.CSimp.instInhabitedEntry = { default := Lean.Compiler.CSimp.instInhabitedEntry.default }

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

Equations

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

structure Lean.Compiler.CSimp.State : Type

• map : SMap Name Entry

  Map from e.fromDeclName to e

• thmNames : SSet Name

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

Equations

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

@[implicit_reducible]

instance Lean.Compiler.CSimp.instInhabitedState : Inhabited State

Equations

• Lean.Compiler.CSimp.instInhabitedState = { default := Lean.Compiler.CSimp.instInhabitedState.default }

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

Equations

• { map := map, thmNames := thmNames }.switch = { map := map.switch, thmNames := thmNames.switch }

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

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

Equations

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

def Lean.Compiler.CSimp.replaceConstant? (env : Environment) (e : Expr) : CoreM (Option Expr)

If e (as a whole) matches a [csimp] theorem, returns the replacement expression.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Compiler.CSimp.replaceConstant? env e = pure none

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

If e (as a whole) matches a [csimp] theorem, returns the replacement expression, or else e.

Equations

• Lean.Compiler.CSimp.replaceConstant env e = do let __do_lift ← Lean.Compiler.CSimp.replaceConstant? env e pure (__do_lift.getD e)

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

Equations

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