Enum LfscTerm 

pub enum LfscTerm {
    Var(String),
    IntLit(i64),
    RatLit(i64, i64),
    True,
    False,
    App(String, Vec<LfscTerm>),
    Lambda(String, Box<LfscSort>, Box<LfscTerm>),
    Pi(String, Box<LfscSort>, Box<LfscTerm>),
    SideCondition(String, Vec<LfscTerm>),
    Hold(Box<LfscTerm>),
    Annotate(Box<LfscTerm>, Box<LfscSort>),
}

An LFSC term

Variants

Var(String)

Variable reference

IntLit(i64)

Integer literal

RatLit(i64, i64)

Rational literal (numerator, denominator)

True

Boolean true

False

Boolean false

App(String, Vec<LfscTerm>)

Application

Lambda(String, Box<LfscSort>, Box<LfscTerm>)

Lambda abstraction

Pi(String, Box<LfscSort>, Box<LfscTerm>)

Pi type (dependent function type)

SideCondition(String, Vec<LfscTerm>)

Side condition application

Hold(Box<LfscTerm>)

Proof hold (assertion)

Annotate(Box<LfscTerm>, Box<LfscSort>)

Type annotation

Trait Implementations

impl Clone for LfscTerm

fn clone(&self) -> LfscTerm

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LfscTerm

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

Formats the value using the given formatter.

impl Display for LfscTerm

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

Formats the value using the given formatter.