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

A named Sym.simp variant. Stores pre/post simproc chains and the discharger for extra theorems 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).

• discharger? : Option Syntax

  Discharger for the side conditions of the extra theorems provided at use time (simp myVariant [thm₁, thm₂, ...]), elaborated at use time. none means no discharge.

• config : Config

  Configuration overrides.

@[instance_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

@[instance_reducible]

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

Equations

• Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry = { default := Lean.Meta.Sym.Simp.instInhabitedSymSimpVariantEntry.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]?