Enum WrapperDriver 

pub enum WrapperDriver {
    List,
    PeanoNat {
        type_name: String,
        value_first: bool,
    },
}

Algebraic / proof-theoretic shape of a verify-law theorem.

Naming rule: variants describe what the law says, not how a backend proves it. The IR is target-agnostic — Lean maps Commutative { op: Add } to simp [fn, Int.add_comm], Dafny maps the same variant to its own lemma vocabulary, a Z3 backend could ship a different tactic again. Tactic names (SimpOverLemmas, simp+omega) do not appear in variant names; Driver of a ProofStrategy::WrapperOverRecursion inner loop — the structure the recursion shrinks. List is the original sum_acc shape (match xs { [] -> acc; h::t -> loop(t, step) }); PeanoNat is the factTR countdown (match n { Z -> acc; S(m) -> loop(m, combine(n, acc)) }). The two need different induction skeletons (nil/cons vs zero/succ) and, for Mul, different closing tactics (omega can’t discharge a nonlinear residual).

Variants

List

Structural fold over a List<_> first parameter.

PeanoNat

Countdown over a Peano-Nat ADT first parameter. Carries the ADT’s source type name and whether the folded value (the matched subject) is the combine fn’s FIRST argument (mul(n, acc) → true; mul(acc, n) → false) so the backend rewrite matches the def’s actual step term.

Fields

type_name: String

value_first: bool

Trait Implementations

impl Clone for WrapperDriver

fn clone(&self) -> WrapperDriver

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for WrapperDriver

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for WrapperDriver

impl PartialEq for WrapperDriver

fn eq(&self, other: &WrapperDriver) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for WrapperDriver