Enum ProofTerm 

pub enum ProofTerm {
    Unit,
    Pair(Box<ProofTerm>, Box<ProofTerm>),
    Fst(Box<ProofTerm>),
    Snd(Box<ProofTerm>),
    Inl(Box<ProofTerm>),
    Inr(Box<ProofTerm>),
    Lambda(String, Box<ProofTerm>),
    App(Box<ProofTerm>, Box<ProofTerm>),
    Pack(String, Box<ProofTerm>),
    Unpack {
        witness: String,
        proof_var: String,
        packed: Box<ProofTerm>,
        body: Box<ProofTerm>,
    },
    Absurd(Box<ProofTerm>),
    Var(String),
}

A proof term in the Curry-Howard correspondence. Each term witnesses a constructive proof of some proposition.

Variants

Unit

Witness for ⊤ (unit).

Pair(Box<ProofTerm>, Box<ProofTerm>)

Witness for P ∧ Q (pair of proofs).

Fst(Box<ProofTerm>)

First projection of a pair (proof of P from proof of P ∧ Q).

Snd(Box<ProofTerm>)

Second projection of a pair (proof of Q from proof of P ∧ Q).

Inl(Box<ProofTerm>)

Left injection into a disjunction (proof of P ∨ Q from proof of P).

Inr(Box<ProofTerm>)

Right injection into a disjunction (proof of P ∨ Q from proof of Q).

Lambda(String, Box<ProofTerm>)

Lambda abstraction (proof of P → Q).

App(Box<ProofTerm>, Box<ProofTerm>)

Function application (modus ponens).

Pack(String, Box<ProofTerm>)

Existential witness packing (pack a witness with a proof).

Unpack

Existential witness unpacking.

Fields

witness: String

The variable binding the witness value.

proof_var: String

The variable binding the proof of the body proposition.

packed: Box<ProofTerm>

The term being unpacked.

body: Box<ProofTerm>

The body using the unpacked witness and proof.

Absurd(Box<ProofTerm>)

Proof by contradiction / ex falso quodlibet from ⊥.

Var(String)

Variable reference.

Trait Implementations

impl Clone for ProofTerm

fn clone(&self) -> ProofTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTerm

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

Formats the value using the given formatter.

impl PartialEq for ProofTerm

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

impl StructuralPartialEq for ProofTerm