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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocPhase = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocPhase.default }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instBEqCbvSimprocPhase = { beq := Lean.Meta.Tactic.Cbv.instBEqCbvSimprocPhase.beq }

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

Equations

• Lean.Meta.Tactic.Cbv.instBEqCbvSimprocPhase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase = { hash := Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase.hash }

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

Equations

• Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase.hash Lean.Meta.Tactic.Cbv.CbvSimprocPhase.pre = 0
• Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase.hash Lean.Meta.Tactic.Cbv.CbvSimprocPhase.eval = 1
• Lean.Meta.Tactic.Cbv.instHashableCbvSimprocPhase.hash Lean.Meta.Tactic.Cbv.CbvSimprocPhase.post = 2

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instReprCbvSimprocPhase = { reprPrec := Lean.Meta.Tactic.Cbv.instReprCbvSimprocPhase.repr }

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

Equations

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

@[instance_reducible]

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

Equations

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

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

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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocOLeanEntry = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocOLeanEntry.default }

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

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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instBEqCbvSimprocEntry = { beq := fun (e₁ e₂ : Lean.Meta.Tactic.Cbv.CbvSimprocEntry) => e₁.declName == e₂.declName }

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instToFormatCbvSimprocEntry = { format := fun (e : Lean.Meta.Tactic.Cbv.CbvSimprocEntry) => Std.format e.declName }

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

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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocs = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocs.default }

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

Equations

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

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

Equations

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

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

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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedBuiltinCbvSimprocs = { default := Lean.Meta.Tactic.Cbv.instInhabitedBuiltinCbvSimprocs.default }

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

Equations

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

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

• declName : Name
• keys : Array DiscrTree.Key

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDecl = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDecl.default }

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

Equations

• d₁.lt d₂ = d₁.declName.quickLt d₂.declName

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

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

@[instance_reducible]

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

Equations

• Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDeclExtState = { default := Lean.Meta.Tactic.Cbv.instInhabitedCbvSimprocDeclExtState.default }

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

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

Equations

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

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

Equations

• Lean.Meta.Tactic.Cbv.isCbvSimproc declName = do let __do_lift ← Lean.Meta.Tactic.Cbv.getCbvSimprocDeclKeys? declName pure __do_lift.isSome

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

Equations

• Lean.Meta.Tactic.Cbv.isBuiltinCbvSimproc declName = do let __do_lift ← Lean.getEnv pure ((Lean.Meta.Tactic.Cbv.cbvSimprocDeclExt.getState __do_lift).builtin.contains declName)

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Tactic.Cbv.CbvSimprocExtension = Lean.ScopedEnvExtension Lean.Meta.Tactic.Cbv.CbvSimprocOLeanEntry Lean.Meta.Tactic.Cbv.CbvSimprocEntry Lean.Meta.Tactic.Cbv.CbvSimprocs

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

Equations

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

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

Equations

• Lean.Meta.Tactic.Cbv.toCbvSimprocEntry e = do let __do_lift ← Lean.Meta.Tactic.Cbv.getCbvSimprocFromDecl e.declName pure { toCbvSimprocOLeanEntry := e, proc := __do_lift }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Tactic.Cbv.addCbvSimprocBuiltinAttr declName phase proc = Lean.Meta.Tactic.Cbv.addCbvSimprocBuiltinAttrCore Lean.Meta.Tactic.Cbv.builtinCbvSimprocsRef declName phase proc

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

Equations

• Lean.Meta.Tactic.Cbv.getCbvSimprocs = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Tactic.Cbv.cbvSimprocExtension __do_lift)

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

Equations

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