Enum ProofStrategy 

pub enum ProofStrategy {
    Auto,
    Induction(String),
    ByRule(String),
    Script(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.

Script(String)

An explicit tactic-script proof, written in the English-esque vernacular and run by the tactic framework. Example: Proof: Assume h. By cases on h, right, by assumption. Left, by assumption.

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<(), Error>

Formats the value using the given formatter.

impl Default for ProofStrategy

fn default() -> ProofStrategy

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