Enum smt2::syntax::ast::Term

pub enum Term {
    Ident(Located<Ident>),
    Let {
        bindings: Vec<Located<Binding>>,
        body: Box<Located<Term>>,
    },
    Forall {
        vars: Vec<Located<SortedVar>>,
        body: Box<Located<Term>>,
    },
    Exists {
        vars: Vec<Located<SortedVar>>,
        body: Box<Located<Term>>,
    },
    Match {
        term: Box<Located<Term>>,
        cases: Vec<Located<MatchCase>>,
    },
    Apply {
        id: Located<Ident>,
        args: Box<Vec<Located<Term>>>,
    },
    Coerce {
        term: Box<Located<Term>>,
        sort: Located<Sort>,
    },
}

::= <spec_const> | ( let ( <var_binding>+ ) ) | ( forall ( <sorted_var>+ ) ) | ( exists ( <sorted_var>+ ) )

Variants

Ident(Located<Ident>)

Let

Fields of Let

bindings: Vec<Located<Binding>>body: Box<Located<Term>>

Forall

Fields of Forall

vars: Vec<Located<SortedVar>>body: Box<Located<Term>>

Exists

Fields of Exists

vars: Vec<Located<SortedVar>>body: Box<Located<Term>>

Match

Fields of Match

term: Box<Located<Term>>cases: Vec<Located<MatchCase>>

Apply

Fields of Apply

id: Located<Ident>args: Box<Vec<Located<Term>>>

Coerce

Fields of Coerce

term: Box<Located<Term>>sort: Located<Sort>

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Display for Term

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

impl Display for Term

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

Formats the value using the given formatter.

impl Parsable for Term

fn parse<L>(lexer: &mut Peekable<L>) -> Result<Located<Term>> where
    L: Iterator<Item = Result<Located<Token>>>, 

Parse from a lexer. Separators are handled depending on the flavor parameter.