Struct Statement 

pub struct Statement {
    pub domain: String,
    pub stem: String,
    pub name: String,
    pub file: String,
    pub sorry_free: bool,
}

One theorem declaration.

Fields

domain: String

stem: String

name: String

file: String

Repo-relative file.

sorry_free: bool

Implementations

impl Statement

pub fn module(&self) -> String

ProvableContracts.Theorems.<Domain>.<File>.

pub fn accepted_names(&self) -> BTreeSet<String>

The names a contract may cite this theorem by — the forms ONT-2a’s scan registers for its theorem, its file and its domain.

Trait Implementations

impl Clone for Statement

fn clone(&self) -> Statement

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Statement

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

Formats the value using the given formatter.

impl Eq for Statement

impl PartialEq for Statement

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Statement