Control Flow Handling for Cbv

Cbv-specific simprocs for ite, dite, cond, match, and Decidable.rec.

The standard Sym.Simp control flow simprocs (simpIte, simpDIte) give up when the condition does not reduce to True or False directly. The Cbv variants (simpIteCbv, simpDIteCbv) go further: they evaluate Decidable.decide on the condition and use eq_true_of_decide / eq_false_of_decide to take the corresponding branch.

def Lean.Meta.Sym.Simp.simpIteCbv : Simproc

Like simpIte but also evaluates Decidable.decide when the condition does not reduce to True/False directly.

Equations

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

def Lean.Meta.Sym.Simp.simpDIteCbv : Simproc

Like simpDIte but also evaluates Decidable.decide when the condition does not reduce to True/False directly.

Equations

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

def Lean.Meta.Tactic.Cbv.withCbvOpaqueGuard {α : Type} (x : MetaM α) : MetaM α

Run a MetaM computation with whnf blocked from unfolding @[cbv_opaque] definitions. This prevents kernel-level reduction (used by reduceRecMatcher? and reduceProj?) from bypassing the @[cbv_opaque] attribute.

Equations

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

def Lean.Meta.Tactic.Cbv.reduceRecMatcher : Sym.Simp.Simproc

Equations

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

def Lean.Meta.Tactic.Cbv.simpControlCbv : Sym.Simp.Simproc

Dispatch control flow constructs to their specialized simprocs. Precondition: e is an application.

Equations

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