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

Equations

• Lean.Meta.Simp.instInhabitedBuiltinSimprocs = { default := Lean.Meta.Simp.instInhabitedBuiltinSimprocs.default }

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

Equations

• Lean.Meta.Simp.instInhabitedSimprocDecl = { default := Lean.Meta.Simp.instInhabitedSimprocDecl.default }

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

Equations

• Lean.Meta.Simp.instInhabitedSimprocDeclExtState = { default := Lean.Meta.Simp.instInhabitedSimprocDeclExtState.default }

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

Equations

• decl₁.lt decl₂ = decl₁.declName.quickLt decl₂.declName

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Simp.isSimproc declName = do let __do_lift ← Lean.Meta.Simp.getSimprocDeclKeys? declName pure __do_lift.isSome

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Simp.registerBuiltinSimproc declName key proc = Lean.Meta.Simp.registerBuiltinSimprocCore declName key (Sum.inl proc)

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

Equations

• Lean.Meta.Simp.registerBuiltinDSimproc declName key proc = Lean.Meta.Simp.registerBuiltinSimprocCore declName key (Sum.inr proc)

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Meta.Simp.instBEqSimprocEntry : BEq SimprocEntry

Equations

• Lean.Meta.Simp.instBEqSimprocEntry = { beq := fun (e₁ e₂ : Lean.Meta.Simp.SimprocEntry) => e₁.declName == e₂.declName }

@[instance_reducible]

instance Lean.Meta.Simp.instToFormatSimprocEntry : ToFormat SimprocEntry

Equations

• Lean.Meta.Simp.instToFormatSimprocEntry = { format := fun (e : Lean.Meta.Simp.SimprocEntry) => Std.format e.declName }

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

Equations

• s.erase declName = { pre := s.pre, post := s.post, simprocNames := Lean.PersistentHashSet.erase s.simprocNames declName, erased := Lean.PersistentHashSet.insert s.erased declName }

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

Equations

• Lean.Meta.Simp.SimprocExtension = Lean.ScopedEnvExtension Lean.Meta.Simp.SimprocOLeanEntry Lean.Meta.Simp.SimprocEntry Lean.Meta.Simprocs

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Simp.toSimprocEntry e = do let __do_lift ← Lean.Meta.Simp.getSimprocFromDecl e.declName pure { toSimprocOLeanEntry := e, proc := __do_lift }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Meta.Simp.addSimprocBuiltinAttr declName post proc = Lean.Meta.Simp.addSimprocBuiltinAttrCore Lean.Meta.Simp.builtinSimprocsRef declName post proc

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

Equations

• Lean.Meta.Simp.addSEvalprocBuiltinAttr declName post proc = Lean.Meta.Simp.addSimprocBuiltinAttrCore Lean.Meta.Simp.builtinSEvalprocsRef declName post proc

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Similar to simprocCore, but for DSimprocs.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocsArray : Type

Equations

• Lean.Meta.Simp.SimprocsArray = Array Lean.Meta.Simprocs

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ss.erase declName = Array.map (fun (s : Lean.Meta.Simprocs) => s.erase declName) ss

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

Equations

• ss.isErased declName = Array.any ss fun (s : Lean.Meta.Simprocs) => Lean.PersistentHashSet.contains s.erased declName

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocExtensionMap : Type

Equations

• Lean.Meta.Simp.SimprocExtensionMap = Std.HashMap Lean.Name Lean.Meta.Simp.SimprocExtension

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

Equations

• One or more equations did not get rendered due to their size.

opaque Lean.Meta.Simp.simprocExtension : SimprocExtension

opaque Lean.Meta.Simp.simprocSEvalExtension : SimprocExtension

def Lean.Meta.Simp.getSimprocs : CoreM Simprocs

Equations

• Lean.Meta.Simp.getSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Simp.simprocExtension __do_lift)

def Lean.Meta.Simp.getSEvalSimprocs : CoreM Simprocs

Equations

• Lean.Meta.Simp.getSEvalSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Simp.simprocSEvalExtension __do_lift)

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

Equations

• Lean.Meta.Simp.getSimprocExtensionCore? attrName = do let __do_lift ← ST.Ref.get Lean.Meta.Simp.simprocExtensionMapRef pure __do_lift[attrName]?

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

Equations

• Lean.Meta.Simp.simpAttrNameToSimprocAttrName attrName = if (attrName == `simp) = true then `simprocAttr else if (attrName == `seval) = true then `sevalprocAttr else attrName.appendAfter "_proc"

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• ext.getSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift)