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.
Instances For
Equations
- Lean.Meta.Simp.instInhabitedBuiltinSimprocs = { default := { keys := default, procs := default } }
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%
.
- declName : Lake.Name
- keys : Array Lean.Meta.SimpTheoremKey
Instances For
Equations
- Lean.Meta.Simp.instInhabitedSimprocDecl = { default := { declName := default, keys := default } }
- builtin : Lean.HashMap Lake.Name (Array Lean.Meta.SimpTheoremKey)
- newEntries : Lean.PHashMap Lake.Name (Array Lean.Meta.SimpTheoremKey)
Instances For
Equations
- Lean.Meta.Simp.instInhabitedSimprocDeclExtState = { default := { builtin := default, newEntries := default } }
Equations
- Lean.Meta.Simp.SimprocDecl.lt decl₁ decl₂ = Lean.Name.quickLt decl₁.declName decl₂.declName
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.isSimproc declName = do let __do_lift ← Lean.Meta.Simp.getSimprocDeclKeys? declName pure (Option.isSome __do_lift)
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.instBEqSimprocEntry = { beq := fun (e₁ e₂ : Lean.Meta.Simp.SimprocEntry) => e₁.toSimprocOLeanEntry.declName == e₂.toSimprocOLeanEntry.declName }
Equations
- Lean.Meta.Simp.instToFormatSimprocEntry = { format := fun (e : Lean.Meta.Simp.SimprocEntry) => Std.format e.toSimprocOLeanEntry.declName }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Builtin symbolic evaluation procedures.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.toSimprocEntry e = do let __do_lift ← Lean.Meta.Simp.getSimprocFromDecl e.declName pure { toSimprocOLeanEntry := e, proc := __do_lift }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Implements attributes builtin_simproc
and builtin_sevalproc
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.addSimprocBuiltinAttr declName post proc = Lean.Meta.Simp.addSimprocBuiltinAttrCore Lean.Meta.Simp.builtinSimprocsRef declName post proc
Instances For
Equations
- Lean.Meta.Simp.addSEvalprocBuiltinAttr declName post proc = Lean.Meta.Simp.addSimprocBuiltinAttrCore Lean.Meta.Simp.builtinSEvalprocsRef declName post proc
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.Simp.getSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Simp.simprocExtension __do_lift)
Instances For
Equations
- Lean.Meta.Simp.getSEvalSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Simp.simprocSEvalExtension __do_lift)
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Equations
- Lean.Meta.Simp.SimprocExtension.getSimprocs ext = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState ext __do_lift)