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_reducible]

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_reducible]

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_reducible]

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_reducible]

instance Lean.Meta.Simp.instBEqSimprocEntry : BEq SimprocEntry

@[instance_reducible]

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

Applies s to e after peeling off numExtraArgs trailing arguments, and re-applies them to the result. This is how a simproc keyed on f a b fires on the over-application f a b c.

numExtraArgs must be the number getMatchWithExtra returned for e itself; a number obtained for a different expression may exceed the number of arguments e has.

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

Runs the applicable simprocs in s on e, and returns as soon as one of them rewrites e.

We must not keep going with the remaining candidates: they were selected for e, and the number of extra arguments recorded for each of them only makes sense for e. The simplifier looks up candidates afresh when it revisits the rewritten expression.

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

Similar to simprocCore, but for DSimprocs.

@[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 (attrName : Name) (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