Struct Obligation 

pub struct Obligation {
    pub name: String,
    pub property: &'static str,
    pub declarations: Vec<Declaration>,
    pub assumptions: Vec<Term>,
    pub conclusion: Term,
    pub origin: Origin,
    pub tier: VerificationTier,
}

A backend-agnostic proof obligation.

Fields

name: String

property: &'static str

declarations: Vec<Declaration>

assumptions: Vec<Term>

conclusion: Term

origin: Origin

tier: VerificationTier

Implementations

impl Obligation

pub fn for_property<P>( name: impl Into<String>, origin: Origin, tier: VerificationTier, conclusion: Term, ) -> Obligation

where P: Property,

Create a new obligation for property P.

pub fn with_decl(self, name: impl Into<String>, sort: Sort) -> Obligation

pub fn with_assumption(self, term: Term) -> Obligation

pub fn associativity( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, ) -> Obligation

Build an associativity obligation for a binary operator symbol.

pub fn associativity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, role: &str, ) -> Obligation

pub fn commutativity( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, ) -> Obligation

Build a commutativity obligation for a binary operator symbol.

pub fn commutativity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, role: &str, ) -> Obligation

pub fn additive_commutativity( name: impl Into<String>, origin: Origin, carrier: Sort, add: impl Into<String>, ) -> Obligation

pub fn additive_commutativity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn monoid_identity( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, identity: impl Into<String>, ) -> Obligation

Build a two-sided identity obligation for a binary operator symbol.

pub fn monoid_identity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn left_identity( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, identity: impl Into<String>, ) -> Obligation

pub fn left_identity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, op_role: &str, identity_role: &str, ) -> Obligation

pub fn right_identity( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, identity: impl Into<String>, ) -> Obligation

pub fn right_identity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, op_role: &str, identity_role: &str, ) -> Obligation

pub fn left_inverse( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, inverse: impl Into<String>, identity: impl Into<String>, ) -> Obligation

pub fn left_inverse_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn right_inverse( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, inverse: impl Into<String>, identity: impl Into<String>, ) -> Obligation

pub fn right_inverse_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn left_distributivity( name: impl Into<String>, origin: Origin, carrier: Sort, add: impl Into<String>, mul: impl Into<String>, ) -> Obligation

pub fn left_distributivity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn right_distributivity( name: impl Into<String>, origin: Origin, carrier: Sort, add: impl Into<String>, mul: impl Into<String>, ) -> Obligation

pub fn right_distributivity_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn idempotency( name: impl Into<String>, origin: Origin, carrier: Sort, op: impl Into<String>, ) -> Obligation

pub fn idempotency_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, role: &str, ) -> Obligation

pub fn absorption( name: impl Into<String>, origin: Origin, carrier: Sort, meet: impl Into<String>, join: impl Into<String>, ) -> Obligation

pub fn absorption_in( name: impl Into<String>, origin: Origin, signature: &AlgebraicSignature, ) -> Obligation

pub fn summary(&self) -> String

Human-readable summary used in debugging and certificate generation.

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<(), Error>

Formats the value using the given formatter.

impl Eq for Obligation

impl From<&Obligation> for LeanTheorem

fn from(obligation: &Obligation) -> LeanTheorem

Converts to this type from the input type.

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 StructuralPartialEq for Obligation