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

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

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 : Lean.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 : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey)
• newEntries : Lean.PHashMap Lean.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₁ decl₂ : Lean.Meta.Simp.SimprocDecl) : Bool

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 : Lean.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 : Lean.Name) : Lean.CoreM Bool

def Lean.Meta.Simp.isSimproc (declName : Lean.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 : Lean.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.

def Lean.Meta.Simp.registerBuiltinSimproc (declName : Lean.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 : Lean.Name) (key : Array Lean.Meta.SimpTheoremKey) (proc : Lean.Meta.Simp.DSimproc) : IO Unit

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

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

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

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

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

@[implemented_by Lean.Meta.Simp.getSimprocFromDeclImpl]

opaque Lean.Meta.Simp.getSimprocFromDecl (declName : Lean.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 : Lean.Name) : Lean.AttrM Unit

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

def Lean.Meta.Simp.Simprocs.addCore (s : Lean.Meta.Simprocs) (keys : Array Lean.Meta.SimpTheoremKey) (declName : Lean.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 : Lean.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 : Lean.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 : Lean.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc) : IO Unit

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

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.

def Lean.Meta.Simp.simprocCore (post : Bool) (s : Lean.Meta.Simp.SimprocTree) (erased : Lean.PHashSet Lean.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 Lean.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.DStep

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocsArray : Type

def Lean.Meta.Simp.SimprocsArray.add (ss : Lean.Meta.Simp.SimprocsArray) (declName : Lean.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 : Lean.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 : Lean.Name) : Bool

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

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

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

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

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

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

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

@[reducible, inline]

abbrev Lean.Meta.Simp.SimprocExtensionMap : Type

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

def Lean.Meta.Simp.registerSimprocAttr (attrName : Lean.Name) (attrDescr : String) (ref? : Option (IO.Ref Lean.Meta.Simprocs)) (name : Lean.Name := by exact decl_name%) : 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

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

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

def Lean.Meta.Simp.getSimprocExtension? (simprocAttrNameOrsimpAttrName : Lean.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.

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