structure Lean.Meta.Simp.BuiltinSimprocs : Type

Builtin simproc declaration extension state.

It contains:

• The discrimination tree keys for each simproc (including symbolic evaluation procedures) name.
• The actual procedure associated with a name.

• keys : Std.HashMap Name (Array SimpTheoremKey)
• procs : Std.HashMap Name (Simproc ⊕ DSimproc)

instance Lean.Meta.Simp.instInhabitedBuiltinSimprocs : Inhabited BuiltinSimprocs

opaque Lean.Meta.Simp.builtinSimprocDeclsRef : IO.Ref BuiltinSimprocs

This global reference is populated using the command builtin_simproc_pattern%.

This reference is then used to process the attributes builtin_simproc and builtin_sevalproc. Both attributes need the keys and the actual procedure registered using the command builtin_simproc_pattern%.

structure Lean.Meta.Simp.SimprocDecl : Type

• declName : Name
• keys : Array SimpTheoremKey

instance Lean.Meta.Simp.instInhabitedSimprocDecl : Inhabited SimprocDecl

structure Lean.Meta.Simp.SimprocDeclExtState : Type

• builtin : Std.HashMap Name (Array SimpTheoremKey)
• newEntries : PHashMap Name (Array SimpTheoremKey)

instance Lean.Meta.Simp.instInhabitedSimprocDeclExtState : Inhabited SimprocDeclExtState

def Lean.Meta.Simp.SimprocDecl.lt (decl₁ decl₂ : SimprocDecl) : Bool

opaque Lean.Meta.Simp.simprocDeclExt : PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState

def Lean.Meta.Simp.getSimprocDeclKeys? (declName : Name) : CoreM (Option (Array SimpTheoremKey))

def Lean.Meta.Simp.isBuiltinSimproc (declName : Name) : CoreM Bool

def Lean.Meta.Simp.isSimproc (declName : Name) : CoreM Bool

def Lean.Meta.Simp.registerBuiltinSimprocCore (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc ⊕ DSimproc) : IO Unit

Given a declaration name declName, store the discrimination tree keys and the actual procedure.

This method is invoked by the command builtin_simproc_pattern% elaborator.

def Lean.Meta.Simp.registerBuiltinSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : Simproc) : IO Unit

def Lean.Meta.Simp.registerBuiltinDSimproc (declName : Name) (key : Array SimpTheoremKey) (proc : DSimproc) : IO Unit

def Lean.Meta.Simp.registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit

instance Lean.Meta.Simp.instBEqSimprocEntry : BEq SimprocEntry

instance Lean.Meta.Simp.instToFormatSimprocEntry : ToFormat SimprocEntry

def Lean.Meta.Simp.Simprocs.erase (s : Simprocs) (declName : Name) : Simprocs

opaque Lean.Meta.Simp.builtinSimprocsRef : IO.Ref Simprocs

Builtin simprocs.

opaque Lean.Meta.Simp.builtinSEvalprocsRef : IO.Ref Simprocs

Builtin symbolic evaluation procedures.

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocExtension : Type

unsafe def Lean.Meta.Simp.getSimprocFromDeclImpl (declName : Name) : ImportM (Simproc ⊕ DSimproc)

@[implemented_by Lean.Meta.Simp.getSimprocFromDeclImpl]

opaque Lean.Meta.Simp.getSimprocFromDecl (declName : Name) : ImportM (Simproc ⊕ DSimproc)

def Lean.Meta.Simp.toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry

def Lean.Meta.Simp.eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit

def Lean.Meta.Simp.addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit

def Lean.Meta.Simp.Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Simproc ⊕ DSimproc) : Simprocs

def Lean.Meta.Simp.addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Simproc ⊕ DSimproc) : IO Unit

Implements attributes builtin_simproc and builtin_sevalproc.

def Lean.Meta.Simp.addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc ⊕ DSimproc) : IO Unit

def Lean.Meta.Simp.addSEvalprocBuiltinAttr (declName : Name) (post : Bool) (proc : Simproc ⊕ DSimproc) : IO Unit

def Lean.Meta.Simp.Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs

def Lean.Meta.Simp.SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step

def Lean.Meta.Simp.SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM DStep

Similar to try, but only consider DSimproc case. That is, if s.proc is a Simproc, treat it as a .continue.

def Lean.Meta.Simp.simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step

def Lean.Meta.Simp.dsimprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM DStep

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocsArray : Type

def Lean.Meta.Simp.SimprocsArray.add (ss : SimprocsArray) (declName : Name) (post : Bool) : CoreM SimprocsArray

def Lean.Meta.Simp.SimprocsArray.erase (ss : SimprocsArray) (declName : Name) : SimprocsArray

def Lean.Meta.Simp.SimprocsArray.isErased (ss : SimprocsArray) (declName : Name) : Bool

def Lean.Meta.Simp.simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step

def Lean.Meta.Simp.dsimprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM DStep

opaque Lean.Meta.Simp.simprocs : Lean.Option Bool

def Lean.Meta.Simp.userPreSimprocs (s : SimprocsArray) : Simproc

def Lean.Meta.Simp.userPostSimprocs (s : SimprocsArray) : Simproc

def Lean.Meta.Simp.userPreDSimprocs (s : SimprocsArray) : DSimproc

def Lean.Meta.Simp.userPostDSimprocs (s : SimprocsArray) : DSimproc

def Lean.Meta.Simp.mkSimprocExt (name : Name := by exact decl_name%) (ref? : Option (IO.Ref Simprocs)) : IO SimprocExtension

def Lean.Meta.Simp.addSimprocAttr (ext : SimprocExtension) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit

def Lean.Meta.Simp.mkSimprocAttr (attrName : Name) (attrDescr : String) (ext : SimprocExtension) (name : Name) : IO Unit

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocExtensionMap : Type

opaque Lean.Meta.Simp.simprocExtensionMapRef : IO.Ref SimprocExtensionMap

def Lean.Meta.Simp.registerSimprocAttr (attrName : Name) (attrDescr : String) (ref? : Option (IO.Ref Simprocs)) (name : Name := by exact decl_name%) : IO SimprocExtension

opaque Lean.Meta.Simp.simprocExtension : SimprocExtension

opaque Lean.Meta.Simp.simprocSEvalExtension : SimprocExtension

def Lean.Meta.Simp.getSimprocs : CoreM Simprocs

def Lean.Meta.Simp.getSEvalSimprocs : CoreM Simprocs

def Lean.Meta.Simp.getSimprocExtensionCore? (attrName : Name) : IO (Option SimprocExtension)

def Lean.Meta.Simp.simpAttrNameToSimprocAttrName (attrName : Name) : Name

def Lean.Meta.Simp.getSimprocExtension? (simprocAttrNameOrsimpAttrName : Name) : IO (Option SimprocExtension)

Try to retrieve the simproc set using the simp or simproc attribute names. Recall that when we declare a simp set using register_simp_attr, an associated simproc set is automatically created. We use the function simpAttrNameToSimprocAttrName to find the simproc associated with the simp attribute.

def Lean.Meta.Simp.SimprocExtension.getSimprocs (ext : SimprocExtension) : CoreM Simprocs