Struct ProofState 

pub struct ProofState {
    pub obligations: Vec<ProofObligation>,
}

A collection of proof obligations, tracking overall proof state.

Fields

obligations: Vec<ProofObligation>

All obligations in this proof attempt.

Implementations

impl ProofState

pub fn new() -> Self

Create a fresh proof state with no obligations.

pub fn add_obligation(&mut self, label: impl Into<String>, proposition: Expr)

Add a new proof obligation.

pub fn remaining(&self) -> usize

Number of obligations that remain undischarged.

pub fn is_complete(&self) -> bool

Whether all obligations are discharged.

pub fn discharge_next(&mut self, proof: Expr) -> bool

Discharge the first undischarged obligation with the given proof.

Returns true if an obligation was discharged, false if all were already done.

pub fn open_obligations(&self) -> Vec<&ProofObligation>

Returns references to all undischarged obligations.

Trait Implementations

impl Clone for ProofState

fn clone(&self) -> ProofState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofState

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

Formats the value using the given formatter.

impl Default for ProofState

fn default() -> ProofState

Returns the “default value” for a type.