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 : Lean.HashMap Lake.Name (Array Lean.Meta.SimpTheoremKey)
• procs : Lean.HashMap Lake.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)

instance Lean.Meta.Simp.instInhabitedBuiltinSimprocs : Inhabited Lean.Meta.Simp.BuiltinSimprocs

Equations

• Lean.Meta.Simp.instInhabitedBuiltinSimprocs = { default := { keys := default, procs := default } }

opaque Lean.Meta.Simp.builtinSimprocDeclsRef : IO.Ref Lean.Meta.Simp.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 : Lake.Name
• keys : Array Lean.Meta.SimpTheoremKey

instance Lean.Meta.Simp.instInhabitedSimprocDecl : Inhabited Lean.Meta.Simp.SimprocDecl

Equations

• Lean.Meta.Simp.instInhabitedSimprocDecl = { default := { declName := default, keys := default } }

structure Lean.Meta.Simp.SimprocDeclExtState : Type

• builtin : Lean.HashMap Lake.Name (Array Lean.Meta.SimpTheoremKey)
• newEntries : Lean.PHashMap Lake.Name (Array Lean.Meta.SimpTheoremKey)

instance Lean.Meta.Simp.instInhabitedSimprocDeclExtState : Inhabited Lean.Meta.Simp.SimprocDeclExtState

Equations

• Lean.Meta.Simp.instInhabitedSimprocDeclExtState = { default := { builtin := default, newEntries := default } }

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

Equations

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

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.isSimproc (declName : Lake.Name) : Lean.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 : Lake.Name) (key : Array Lean.Meta.SimpTheoremKey) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.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 : Lake.Name) (key : Array Lean.Meta.SimpTheoremKey) (proc : Lean.Meta.Simp.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 : Lake.Name) (key : Array Lean.Meta.SimpTheoremKey) (proc : Lean.Meta.Simp.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 : Lake.Name) (keys : Array Lean.Meta.SimpTheoremKey) : Lean.CoreM Unit

Equations

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

instance Lean.Meta.Simp.instBEqSimprocEntry : BEq Lean.Meta.Simp.SimprocEntry

Equations

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

instance Lean.Meta.Simp.instToFormatSimprocEntry : Lean.ToFormat Lean.Meta.Simp.SimprocEntry

Equations

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

def Lean.Meta.Simp.Simprocs.erase (s : Lean.Meta.Simprocs) (declName : Lake.Name) : Lean.Meta.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 Lean.Meta.Simprocs

Builtin simprocs.

opaque Lean.Meta.Simp.builtinSEvalprocsRef : IO.Ref Lean.Meta.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 : Lake.Name) : Lean.ImportM (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.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 : Lake.Name) : Lean.ImportM (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)

def Lean.Meta.Simp.toSimprocEntry (e : Lean.Meta.Simp.SimprocOLeanEntry) : Lean.ImportM Lean.Meta.Simp.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 : Lean.Meta.Simp.SimprocExtension) (declName : Lake.Name) : Lean.AttrM Unit

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.addSimprocBuiltinAttrCore (ref : IO.Ref Lean.Meta.Simprocs) (declName : Lake.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.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 : Lake.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.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 : Lake.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.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 : Lean.Meta.Simprocs) (declName : Lake.Name) (post : Bool) : Lean.CoreM Lean.Meta.Simprocs

Equations

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

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

Equations

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

def Lean.Meta.Simp.SimprocEntry.tryD (s : Lean.Meta.Simp.SimprocEntry) (numExtraArgs : Nat) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.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 : Lean.Meta.Simp.SimprocTree) (erased : Lean.PHashSet Lake.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

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

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 : Lean.Meta.Simp.SimprocsArray) (declName : Lake.Name) (post : Bool) : Lean.CoreM Lean.Meta.Simp.SimprocsArray

Equations

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

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

Equations

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

def Lean.Meta.Simp.SimprocsArray.isErased (ss : Lean.Meta.Simp.SimprocsArray) (declName : Lake.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 : Lean.Meta.Simp.SimprocsArray) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.Simp.dsimprocArrayCore (post : Bool) (ss : Lean.Meta.Simp.SimprocsArray) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.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 : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Simproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.mkSimprocExt (name : autoParam Lake.Name _auto✝) (ref? : Option (IO.Ref Lean.Meta.Simprocs)) : IO Lean.Meta.Simp.SimprocExtension

Equations

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

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

Equations

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

def Lean.Meta.Simp.mkSimprocAttr (attrName : Lake.Name) (attrDescr : String) (ext : Lean.Meta.Simp.SimprocExtension) (name : Lake.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 = Lean.HashMap Lake.Name Lean.Meta.Simp.SimprocExtension

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

def Lean.Meta.Simp.registerSimprocAttr (attrName : Lake.Name) (attrDescr : String) (ref? : Option (IO.Ref Lean.Meta.Simprocs)) (name : autoParam Lake.Name _auto✝) : IO Lean.Meta.Simp.SimprocExtension

Equations

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

opaque Lean.Meta.Simp.simprocExtension : Lean.Meta.Simp.SimprocExtension

opaque Lean.Meta.Simp.simprocSEvalExtension : Lean.Meta.Simp.SimprocExtension

def Lean.Meta.Simp.getSimprocs : Lean.CoreM Lean.Meta.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 : Lean.CoreM Lean.Meta.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 : Lake.Name) : IO (Option Lean.Meta.Simp.SimprocExtension)

Equations

• Lean.Meta.Simp.getSimprocExtensionCore? attrName = do let __do_lift ← ST.Ref.get Lean.Meta.Simp.simprocExtensionMapRef pure (Lean.HashMap.find? __do_lift attrName)

def Lean.Meta.Simp.simpAttrNameToSimprocAttrName (attrName : Lake.Name) : Lake.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 : Lake.Name) : IO (Option Lean.Meta.Simp.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 : Lean.Meta.Simp.SimprocExtension) : Lean.CoreM Lean.Meta.Simprocs

Equations

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