Documentation

Lean.Meta.Tactic.Cbv.ControlFlow

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.

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

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

Instances For
    source
    def Lean.Meta.Sym.Simp.simpDIteCbv :
    Simproc

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

    Instances For
      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.

      Instances For
        source
        def Lean.Meta.Tactic.Cbv.reduceRecMatcher :
        Sym.Simp.Simproc
        Instances For
          source
          def Lean.Meta.Tactic.Cbv.simpControlCbv :
          Sym.Simp.Simproc

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

          Instances For