structure Lean.Meta.Sym.Simp.SymSimpVariant : Type

A named Sym.simp variant. Stores pre/post simproc chains as syntax (elaborated at use time in GrindTacticM) and configuration overrides.

• pre? : Option Syntax

  Pre-processing simproc chain (elaborated at use time).

• post? : Option Syntax

  Post-processing simproc chain (elaborated at use time).

• config : Config

  Configuration overrides.

def Lean.Meta.Sym.Simp.instInhabitedSymSimpVariant.default : SymSimpVariant

Equations

• Lean.Meta.Sym.Simp.instInhabitedSymSimpVariant.default = { pre? := default, post? := default, config := default }

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedSymSimpVariant : Inhabited SymSimpVariant

Equations

• Lean.Meta.Sym.Simp.instInhabitedSymSimpVariant = { default := Lean.Meta.Sym.Simp.instInhabitedSymSimpVariant.default }

structure Lean.Meta.Sym.Simp.SymSimpVariantEntry : Type

Entry for the scoped environment extension.

• name : Name
• variant : SymSimpVariant

@[implicit_reducible]

instance Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry : Inhabited SymSimpVariantEntry

Equations

• Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry = { default := Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry.default }

def Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry.default : SymSimpVariantEntry

Equations

• Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry.default = { name := default, variant := default }

opaque Lean.Meta.Sym.Simp.symSimpVariantExtension : SimpleScopedEnvExtension SymSimpVariantEntry (Std.HashMap Name SymSimpVariant)

Persistent environment extension mapping variant names to their definitions.

def Lean.Meta.Sym.Simp.getSymSimpVariant? (env : Environment) (name : Name) : Option SymSimpVariant

Look up a named Sym.simp variant.

Equations

• Lean.Meta.Sym.Simp.getSymSimpVariant? env name = (Lean.ScopedEnvExtension.getState Lean.Meta.Sym.Simp.symSimpVariantExtension env)[name]?