Enum 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>+ ) <term> )

•   	| ( forall ( <sorted_var>+ ) <term> )

•   	| ( exists ( <sorted_var>+ ) <term> )

Variants

Ident(Located<Ident>)

Let

Fields

bindings: Vec<Located<Binding>>

body: Box<Located<Term>>

Forall

Fields

vars: Vec<Located<SortedVar>>

body: Box<Located<Term>>

Exists

Fields

vars: Vec<Located<SortedVar>>

body: Box<Located<Term>>

Match

Fields

term: Box<Located<Term>>

cases: Vec<Located<MatchCase>>

Apply

Fields

id: Located<Ident>

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

Coerce

Fields

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

Formats the value using the given formatter.

impl Display for Term

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

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.