inductive Lean.Meta.Tactic.Cbv.CbvSimprocPhase : Type

The phase at which a cbv_simproc fires during cbv normalization.

• pre (↓): Fires on each subexpression before cbv reduction, so arguments are still unreduced. Runs before cbv-specific pre-steps (projection reduction, unfolding, etc.).
• eval (cbv_eval): Fires during the post phase, after ground evaluation but before handleApp attempts equation lemmas, unfolding, and recursion reduction. Arguments have already been reduced.
• post (↑, default): Fires during the post phase, after handleApp has attempted standard reduction. Arguments have already been reduced.

• pre : CbvSimprocPhase
• eval : CbvSimprocPhase
• post : CbvSimprocPhase

def Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocPhase.default : CbvSimprocPhase

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocPhase : Inhabited CbvSimprocPhase

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instBEqCbvSimprocPhase : BEq CbvSimprocPhase

def Lean.Meta.Tactic.Cbv.instBEqCbvSimprocPhase.beq : CbvSimprocPhase → CbvSimprocPhase → Bool

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase : Hashable CbvSimprocPhase

def Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase.hash : CbvSimprocPhase → UInt64

def Lean.Meta.Tactic.Cbv.instReprCbvSimprocPhase.repr : CbvSimprocPhase → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instReprCbvSimprocPhase : Repr CbvSimprocPhase

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instToExprCbvSimprocPhase : ToExpr CbvSimprocPhase

structure Lean.Meta.Tactic.Cbv.CbvSimprocOLeanEntry : Type

• declName : Name
• phase : CbvSimprocPhase
• keys : Array DiscrTree.Key

def Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocOLeanEntry.default : CbvSimprocOLeanEntry

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocOLeanEntry : Inhabited CbvSimprocOLeanEntry

structure Lean.Meta.Tactic.Cbv.CbvSimprocEntryextends Lean.Meta.Tactic.Cbv.CbvSimprocOLeanEntry : Type

• declName : Name
• phase : CbvSimprocPhase
• keys : Array DiscrTree.Key
• proc : Sym.Simp.Simproc

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instBEqCbvSimprocEntry : BEq CbvSimprocEntry

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instToFormatCbvSimprocEntry : ToFormat CbvSimprocEntry

structure Lean.Meta.Tactic.Cbv.CbvSimprocs : Type

• pre : DiscrTree CbvSimprocEntry
• eval : DiscrTree CbvSimprocEntry
• post : DiscrTree CbvSimprocEntry
• simprocNames : PHashSet Name
• erased : PHashSet Name

def Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocs.default : CbvSimprocs

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocs : Inhabited CbvSimprocs

def Lean.Meta.Tactic.Cbv.CbvSimprocs.addCore (s : CbvSimprocs) (keys : Array DiscrTree.Key) (declName : Name) (phase : CbvSimprocPhase) (proc : Sym.Simp.Simproc) : CbvSimprocs

def Lean.Meta.Tactic.Cbv.CbvSimprocs.erase (s : CbvSimprocs) (declName : Name) : CbvSimprocs

structure Lean.Meta.Tactic.Cbv.BuiltinCbvSimprocs : Type

• keys : Std.HashMap Name (Array DiscrTree.Key)
• procs : Std.HashMap Name Sym.Simp.Simproc

def Lean.Meta.Tactic.Cbv.instInhabitedBuiltinCbvSimprocs.default : BuiltinCbvSimprocs

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedBuiltinCbvSimprocs : Inhabited BuiltinCbvSimprocs

opaque Lean.Meta.Tactic.Cbv.builtinCbvSimprocDeclsRef : IO.Ref BuiltinCbvSimprocs

def Lean.Meta.Tactic.Cbv.registerBuiltinCbvSimproc (declName : Name) (keys : Array DiscrTree.Key) (proc : Sym.Simp.Simproc) : IO Unit

structure Lean.Meta.Tactic.Cbv.CbvSimprocDecl : Type

• declName : Name
• keys : Array DiscrTree.Key

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDecl : Inhabited CbvSimprocDecl

def Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDecl.default : CbvSimprocDecl

def Lean.Meta.Tactic.Cbv.CbvSimprocDecl.lt (d₁ d₂ : CbvSimprocDecl) : Bool

structure Lean.Meta.Tactic.Cbv.CbvSimprocDeclExtState : Type

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

@[implicit_reducible]

instance Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDeclExtState : Inhabited CbvSimprocDeclExtState

def Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDeclExtState.default : CbvSimprocDeclExtState

opaque Lean.Meta.Tactic.Cbv.cbvSimprocDeclExt : PersistentEnvExtension CbvSimprocDecl CbvSimprocDecl CbvSimprocDeclExtState

def Lean.Meta.Tactic.Cbv.getCbvSimprocDeclKeys? (declName : Name) : CoreM (Option (Array DiscrTree.Key))

def Lean.Meta.Tactic.Cbv.isCbvSimproc (declName : Name) : CoreM Bool

def Lean.Meta.Tactic.Cbv.isBuiltinCbvSimproc (declName : Name) : CoreM Bool

def Lean.Meta.Tactic.Cbv.registerCbvSimproc (declName : Name) (keys : Array DiscrTree.Key) : CoreM Unit

@[reducible, inline]

abbrev Lean.Meta.Tactic.Cbv.CbvSimprocExtension : Type

unsafe def Lean.Meta.Tactic.Cbv.getCbvSimprocFromDeclImpl (declName : Name) : ImportM Sym.Simp.Simproc

@[implemented_by Lean.Meta.Tactic.Cbv.getCbvSimprocFromDeclImpl]

opaque Lean.Meta.Tactic.Cbv.getCbvSimprocFromDecl (declName : Name) : ImportM Sym.Simp.Simproc

def Lean.Meta.Tactic.Cbv.toCbvSimprocEntry (e : CbvSimprocOLeanEntry) : ImportM CbvSimprocEntry

opaque Lean.Meta.Tactic.Cbv.builtinCbvSimprocsRef : IO.Ref CbvSimprocs

opaque Lean.Meta.Tactic.Cbv.cbvSimprocExtension : CbvSimprocExtension

def Lean.Meta.Tactic.Cbv.eraseCbvSimprocAttr (declName : Name) : AttrM Unit

def Lean.Meta.Tactic.Cbv.addCbvSimprocAttrCore (declName : Name) (kind : AttributeKind) (phase : CbvSimprocPhase) : CoreM Unit

def Lean.Meta.Tactic.Cbv.parseCbvSimprocPhase (stx : Syntax) : CbvSimprocPhase

def Lean.Meta.Tactic.Cbv.addCbvSimprocAttr (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit

def Lean.Meta.Tactic.Cbv.addCbvSimprocBuiltinAttrCore (ref : IO.Ref CbvSimprocs) (declName : Name) (phase : CbvSimprocPhase) (proc : Sym.Simp.Simproc) : IO Unit

def Lean.Meta.Tactic.Cbv.addCbvSimprocBuiltinAttr (declName : Name) (phase : CbvSimprocPhase) (proc : Sym.Simp.Simproc) : IO Unit

def Lean.Meta.Tactic.Cbv.getCbvSimprocs : CoreM CbvSimprocs

def Lean.Meta.Tactic.Cbv.cbvSimprocDispatch (tree : DiscrTree CbvSimprocEntry) (erased : PHashSet Name) : Sym.Simp.Simproc