Enum minitt::syntax::Expression

pub enum Expression {
    Unit,
    One,
    Type,
    Void,
    Var(String),
    Sum(Branch),
    Function(Branch),
    Pi(Pattern, Box<Self>, Box<Self>),
    Sigma(Pattern, Box<Self>, Box<Self>),
    Lambda(Pattern, Box<Self>),
    First(Box<Self>),
    Second(Box<Self>),
    Application(Box<Self>, Box<Self>),
    Pair(Box<Self>, Box<Self>),
    Constructor(String, Box<Self>),
    Declaration(Box<Declaration>, Box<Self>),
}

Exp in Mini-TT. Expression language for Mini-TT.

Variants

UnitOneTypeVoidVar(String)Sum(Branch)Function(Branch)Pi(Pattern, Box<Self>, Box<Self>)Sigma(Pattern, Box<Self>, Box<Self>)Lambda(Pattern, Box<Self>)First(Box<Self>)Second(Box<Self>)Application(Box<Self>, Box<Self>)Pair(Box<Self>, Box<Self>)Constructor(String, Box<Self>)Declaration(Box<Declaration>, Box<Self>)

Methods

impl Expression

pub fn eval(self, context: Telescope) -> Value

eval in Mini-TT.
Evaluate an Expression to a Value under a Telescope, panic if not well-typed.

Trait Implementations

impl PartialEq<Expression> for Expression

fn eq(&self, other: &Expression) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Expression) -> bool

This method tests for !=.

impl Ord for Expression

fn cmp(&self, other: &Expression) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

impl Clone for Expression

fn clone(&self) -> Expression

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Eq for Expression

impl PartialOrd<Expression> for Expression

fn partial_cmp(&self, other: &Expression) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Expression) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Expression) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Expression) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Expression) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl Display for Expression

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

Formats the value using the given formatter.

impl Debug for Expression

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

Formats the value using the given formatter.