Struct Obligation 

pub struct Obligation {
    pub lemmas: Vec<Lemma>,
    pub compared: usize,
    pub identical: usize,
    pub assumed: Vec<String>,
    /* private fields */
}

What two graphs give a solver. A tensor both keep that the two graphs compute by one term needs no proof; one they compute by different terms is equal when the open functions are applied to equal operands, down to the pairs of terms that differ in more than their operands — an index map, a store, a value only one side computes. Each such pair is a lemma, its terms defined down to the subterms both share, which stand for any values; so is every read of the rewritten graph that its facts must keep in range.

Fields

lemmas: Vec<Lemma>

What the proof checks beyond the terms both graphs share.

compared: usize

The tensors compared: every one both graphs keep that an op of either writes.

identical: usize

Of those, the ones both graphs compute by the same term.

assumed: Vec<String>

The facts the lemmas assume, each saying what states it.

Implementations

impl Obligation

pub fn text(&self) -> String

The tensors compared and every lemma, as one text: what a proof of it is a proof of.

pub fn digest(&self) -> String

The text’s sha256, as 64 lowercase hex digits.

Trait Implementations

impl Clone for Obligation

fn clone(&self) -> Obligation

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Obligation

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

Formats the value using the given formatter.

impl PartialEq for Obligation

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

impl StructuralPartialEq for Obligation