Trait Proof 

pub trait Proof {
    type Proves: Formula;

    const LENGTH: usize;

    // Required method
    fn display_offset(start_line_num: usize) -> String;

    // Provided method
    fn display() -> String { ... }
}

A sequence of statements that prove a formula.

See the module documentation for more info.

Required Associated Constants

const LENGTH: usize

How many statements this proof involves.

Required Associated Types

type Proves: Formula

The formula that this proof proves.

Required Methods

fn display_offset(start_line_num: usize) -> String

Displays the proof as a string, with line numbers starting from start_line_num.

Provided Methods

fn display() -> String

Displays the proof as a string.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<A> Proof for A

where A: Axiom,

const LENGTH: usize = 1usize

type Proves = A

impl<P, Q, PrP, PrI> Proof for MP<PrP, PrI>

where P: Formula, Q: Formula, PrP: Proof<Proves = P>, PrI: Proof<Proves = Implies<P, Q>>,

const LENGTH: usize

type Proves = Q