Struct TranslationObligation 

pub struct TranslationObligation {
    pub source: String,
    pub target: String,
    pub kind: String,
    pub closed_goal: bool,
    pub discharge: String,
    pub check: Option<String>,
}

How a proof obligation of the source is met in the target.

Fields

source: String

Source theorem, or main:assert@<offset> for an assertion.

target: String

Target declaration that states it.

kind: String

theorem or assertion.

closed_goal: bool

Whether the statement has no free variables.

discharge: String

target-kernel, source-kernel or runtime-assertion.

check: Option<String>

The target-side check of a source-kernel proof (bounded).

Trait Implementations

impl Clone for TranslationObligation

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 TranslationObligation

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

Formats the value using the given formatter.

impl Eq for TranslationObligation

impl PartialEq for TranslationObligation

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for TranslationObligation