Struct ConstructiveProof 

pub struct ConstructiveProof {
    pub statement: String,
    pub algorithm: String,
}

A constructive proof of a statement, given as an explicit algorithm.

Fields

statement: String

The statement being proved.

algorithm: String

The algorithm (witness / proof term) realising the statement.

Implementations

impl ConstructiveProof

pub fn new(statement: impl Into<String>, algorithm: impl Into<String>) -> Self

Create a new constructive proof.

pub fn is_effective(&self) -> bool

A proof is effective if the algorithm terminates on every input.

pub fn witnesses_existential(&self) -> bool

If the statement is existential, does this proof provide a witness?