source
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)

Instances For

source
def Lean.Meta.Simp.instInhabitedBuiltinSimprocs.default :
BuiltinSimprocs
Equations

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

Instances For

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

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

source
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%`.

source
structure Lean.Meta.Simp.SimprocDecl :
Type

- declName : Name
- keys : Array SimpTheoremKey

Instances For

source
def Lean.Meta.Simp.instInhabitedSimprocDecl.default :
SimprocDecl
Equations

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

Instances For

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

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

source
structure Lean.Meta.Simp.SimprocDeclExtState :
Type

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

Instances For

source
def Lean.Meta.Simp.instInhabitedSimprocDeclExtState.default :
SimprocDeclExtState
Equations

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

Instances For

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

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

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

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

Instances For

source
opaque Lean.Meta.Simp.simprocDeclExt :
PersistentEnvExtension SimprocDecl SimprocDecl SimprocDeclExtState
source
def Lean.Meta.Simp.getSimprocDeclKeys? (declName : Name) :
CoreM (Option (Array SimpTheoremKey))
Equations

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

Instances For

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

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

Instances For

source
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

Instances For

source
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.

Instances For

source
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)

Instances For

source
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)

Instances For

source
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.

Instances For

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

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

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

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

source
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 }

Instances For

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

Builtin simprocs.

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

Builtin symbolic evaluation procedures.

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

Instances For

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

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

Instances For

source
@[implemented_by Lean.Meta.Simp.getSimprocFromDeclImpl]
opaque Lean.Meta.Simp.getSimprocFromDecl (declName : Name) :
ImportM (Simproc ⊕ DSimproc)
source
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 }

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

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

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

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.SimprocsArray :
Type
Equations

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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
opaque Lean.Meta.Simp.simprocs :
Lean.Option Bool
source
def Lean.Meta.Simp.userPreSimprocs (s : SimprocsArray) :
Simproc
Equations

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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.

Instances For

source
@[reducible, inline]
abbrev Lean.Meta.Simp.SimprocExtensionMap :
Type
Equations

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

Instances For

source
opaque Lean.Meta.Simp.simprocExtensionMapRef :
IO.Ref SimprocExtensionMap
source
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.

Instances For

source
opaque Lean.Meta.Simp.simprocExtension :
SimprocExtension
source
opaque Lean.Meta.Simp.simprocSEvalExtension :
SimprocExtension
source
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)

Instances For

source
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)

Instances For

source
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]?

Instances For

source
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"

Instances For

source
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.

Instances For

source
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)

Instances For