Documentation

Lean.Meta.Tactic.Cbv.ControlFlow

Control Flow Handling for Cbv #

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

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.

source
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.
Instances For
    source
    def Lean.Meta.Tactic.Cbv.reduceRecMatcher :
    Sym.Simp.Simproc
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Tactic.Cbv.tryMatcher :
      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.
      Instances For