Enum ProofStrategy 

pub enum ProofStrategy {
    Auto,
    Induction(String),
    ByRule(String),
}

Proof strategies for theorem verification.

Variants

Auto

Automatic proof search using backward chaining. The prover will try all available inference rules.

Induction(String)

Induction on a variable (for inductive types like Nat, List). Example: Proof: Induction on n.

ByRule(String)

Direct application of a specific rule. Example: Proof: ModusPonens.

Trait Implementations

impl Clone for ProofStrategy

fn clone(&self) -> ProofStrategy

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofStrategy

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

Formats the value using the given formatter.

impl Default for ProofStrategy

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq for ProofStrategy

fn eq(&self, other: &ProofStrategy) -> 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 ProofStrategy