Enum Term 

pub enum Term {
    Var(String),
    Bool(bool),
    Int(i64),
    App {
        function: String,
        args: Vec<Term>,
    },
    Eq(Box<Term>, Box<Term>),
    And(Vec<Term>),
    Or(Vec<Term>),
    Not(Box<Term>),
    Implies(Box<Term>, Box<Term>),
}

Backend-agnostic term language for proof obligations.

Variants

Var(String)

Bool(bool)

Int(i64)

App

Fields

function: String

args: Vec<Term>

Eq(Box<Term>, Box<Term>)

And(Vec<Term>)

Or(Vec<Term>)

Not(Box<Term>)

Implies(Box<Term>, Box<Term>)

Implementations

impl Term

pub fn var(name: impl Into<String>) -> Term

pub fn bool(value: bool) -> Term

pub fn int(value: i64) -> Term

pub fn app( function: impl Into<String>, args: impl IntoIterator<Item = Term>, ) -> Term

pub fn eq(left: Term, right: Term) -> Term

pub fn and(terms: impl IntoIterator<Item = Term>) -> Term

pub fn or(terms: impl IntoIterator<Item = Term>) -> Term

pub fn negate(term: Term) -> Term

pub fn implies(lhs: Term, rhs: Term) -> Term

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Term

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

Formats the value using the given formatter.

impl PartialEq for Term

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

impl StructuralPartialEq for Term