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

• Lean.Meta.Simp.instInhabitedBuiltinSimprocs

instance Lean.Meta.Simp.instInhabitedBuiltinSimprocs : Inhabited BuiltinSimprocs

Equations

• Lean.Meta.Simp.instInhabitedBuiltinSimprocs = { default := { keys := default, procs := 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

Instances For

• Lean.Meta.Simp.instInhabitedSimprocDecl

instance Lean.Meta.Simp.instInhabitedSimprocDecl : Inhabited SimprocDecl

Equations

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

structure Lean.Meta.Simp.SimprocDeclExtState : Type

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

Instances For

• Lean.Meta.Simp.instInhabitedSimprocDeclExtState

instance Lean.Meta.Simp.instInhabitedSimprocDeclExtState : Inhabited SimprocDeclExtState

Equations

• Lean.Meta.Simp.instInhabitedSimprocDeclExtState = { default := { builtin := default, newEntries := 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 Lean.Meta.Simp.instBEqSimprocEntry : BEq SimprocEntry

Equations

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

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

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

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

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