structure Lean.Meta.Sym.DSimp.SymDSimpVariant : Type

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

• pre? : Option Syntax

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

• post? : Option Syntax

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

• config : Config

  Configuration overrides.

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariant : Inhabited SymDSimpVariant

Equations

• Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariant = { default := Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariant.default }

structure Lean.Meta.Sym.DSimp.SymDSimpVariantEntry : Type

Entry for the scoped environment extension.

• name : Name
• variant : SymDSimpVariant

@[implicit_reducible]

instance Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariantEntry : Inhabited SymDSimpVariantEntry

Equations

• Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariantEntry = { default := Lean.Meta.Sym.DSimp.instInhabitedSymDSimpVariantEntry.default }

opaque Lean.Meta.Sym.DSimp.symDSimpVariantExtension : SimpleScopedEnvExtension SymDSimpVariantEntry (Std.HashMap Name SymDSimpVariant)

Persistent environment extension mapping variant names to their definitions.

def Lean.Meta.Sym.DSimp.getSymDSimpVariant? (env : Environment) (name : Name) : Option SymDSimpVariant

Look up a named Sym.dsimp variant.

Equations

• Lean.Meta.Sym.DSimp.getSymDSimpVariant? env name = (Lean.ScopedEnvExtension.getState Lean.Meta.Sym.DSimp.symDSimpVariantExtension env)[name]?