Lean.Meta.Tactic.Simp.Simproc

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

Instances For

source

instance Lean.Meta.Simp.instInhabitedBuiltinSimprocs :

Inhabited Lean.Meta.Simp.BuiltinSimprocs

Equations

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

source

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

source

structure Lean.Meta.Simp.SimprocDecl :

Type

declName : Lake.Name
keys : Array Lean.Meta.SimpTheoremKey

Instances For

source

instance Lean.Meta.Simp.instInhabitedSimprocDecl :

Inhabited Lean.Meta.Simp.SimprocDecl

Equations

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

source

structure Lean.Meta.Simp.SimprocDeclExtState :

Type

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

Instances For

source

instance Lean.Meta.Simp.instInhabitedSimprocDeclExtState :

Inhabited Lean.Meta.Simp.SimprocDeclExtState

Equations

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

source

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

Bool

Equations

Lean.Meta.Simp.SimprocDecl.lt decl₁ decl₂ = Lean.Name.quickLt decl₁.declName decl₂.declName

Instances For

source

opaque Lean.Meta.Simp.simprocDeclExt :

Lean.PersistentEnvExtension Lean.Meta.Simp.SimprocDecl Lean.Meta.Simp.SimprocDecl Lean.Meta.Simp.SimprocDeclExtState

source

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.

Instances For

source

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

Lean.CoreM Bool

Equations

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

Instances For

source

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 (Option.isSome __do_lift)

Instances For

source

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

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

Instances For

source

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 }

source

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 }

source

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

Lean.Meta.Simprocs

Equations

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

Instances For

source

opaque Lean.Meta.Simp.builtinSimprocsRef :

IO.Ref Lean.Meta.Simprocs

Builtin simprocs.

source

opaque Lean.Meta.Simp.builtinSEvalprocsRef :

IO.Ref Lean.Meta.Simprocs

Builtin symbolic evaluation procedures.

source

@[inline, reducible]

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 : Lake.Name) :

Lean.ImportM Lean.Meta.Simp.Simproc

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 : Lake.Name) :

Lean.ImportM Lean.Meta.Simp.Simproc

source

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 }

Instances For

source

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.

Instances For

source

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.

Instances For

source

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

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 : Lake.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc) :

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 : Lake.Name) (post : Bool) (proc : Lean.Meta.Simp.Simproc) :

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

Instances For

source

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.

Instances For

source

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.

Instances For

source

@[inline, reducible]

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

Instances For

source

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

Lean.Meta.Simp.SimprocsArray

Equations

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

Instances For

source

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

Bool

Equations

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

Instances For

source

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.

Instances For

source

opaque Lean.Meta.Simp.simprocs :

Lean.Option Bool

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

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.

Instances For

source

@[inline, reducible]

abbrev Lean.Meta.Simp.SimprocExtensionMap :

Type

Equations

Lean.Meta.Simp.SimprocExtensionMap = Lean.HashMap Lake.Name Lean.Meta.Simp.SimprocExtension

Instances For

source

opaque Lean.Meta.Simp.simprocExtensionMapRef :

IO.Ref Lean.Meta.Simp.SimprocExtensionMap

source

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.

Instances For

source

opaque Lean.Meta.Simp.simprocExtension :

Lean.Meta.Simp.SimprocExtension

source

opaque Lean.Meta.Simp.simprocSEvalExtension :

Lean.Meta.Simp.SimprocExtension

source

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)

Instances For

source

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)

Instances For

source

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)

Instances For

source

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

Lake.Name

Equations

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

Instances For

source

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.

Instances For

source

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

Lean.CoreM Lean.Meta.Simprocs

Equations

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

Instances For