Documentation

Lean.Compiler.CSimpAttr

structure Lean.Compiler.CSimp.Entry :

Type

fromDeclName : Lean.Name
toDeclName : Lean.Name

instance Lean.Compiler.CSimp.instInhabitedEntry :

Inhabited Lean.Compiler.CSimp.Entry

Equations

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

@[inline]

abbrev Lean.Compiler.CSimp.State :

Type

Equations

Lean.Compiler.CSimp.State = Lean.SMap Lean.Name Lean.Name

constant 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

Lean.Compiler.CSimp.add declName kind = do let a ← Lean.Compiler.CSimp.isConstantReplacement? declName match a with | some entry => Lean.ScopedEnvExtension.add Lean.Compiler.CSimp.ext entry kind | x => Lean.throwError (Lean.toMessageData "invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported.")

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

Equations

Lean.Compiler.CSimp.replaceConstants env e = let map := Lean.ScopedEnvExtension.getState Lean.Compiler.CSimp.ext env; Lean.Expr.replace (fun e => if Lean.Expr.isConst e = true then match Lean.SMap.find? map (Lean.Expr.constName! e) with | some declNameNew => some (Lean.mkConst declNameNew (Lean.Expr.constLevels! e)) | none => none else none) e