Struct ProofObligation 

pub struct ProofObligation {
    pub label: String,
    pub proposition: Expr,
    pub discharged: bool,
    pub proof_term: Option<Expr>,
}

Represents a single obligation in a proof: a goal that must be closed.

Fields

label: String

A human-readable label for this obligation.

proposition: Expr

The proposition that must be proved.

discharged: bool

Whether this obligation has been discharged.

proof_term: Option<Expr>

The proof term supplied, if any.

Implementations

impl ProofObligation

pub fn new(label: impl Into<String>, proposition: Expr) -> Self

Create a new undischarged obligation.

pub fn discharge(&mut self, proof: Expr)

Discharge this obligation with a given proof term.

pub fn is_discharged(&self) -> bool

Returns true if this obligation has been discharged.

Trait Implementations

impl Clone for ProofObligation

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofObligation

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

Formats the value using the given formatter.