Enum minitt::syntax::Expression

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

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

Variants

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

Methods

impl<Name: DebuggableNameTrait> Expression<Name>

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

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

Trait Implementations

impl<Name: PartialEq + NameTrait> PartialEq<Expression<Name>> for Expression<Name>

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

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

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

This method tests for !=.

impl<Name: Clone + NameTrait> Clone for Expression<Name>

fn clone(&self) -> Expression<Name>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Name: PartialOrd + NameTrait> PartialOrd<Expression<Name>> for Expression<Name>

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

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

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

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

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

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

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

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

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

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

impl<Name: Eq + NameTrait> Eq for Expression<Name>

impl<Name: Ord + NameTrait> Ord for Expression<Name>

fn cmp(&self, other: &Expression<Name>) -> 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<Name: Debug + NameTrait> Debug for Expression<Name>

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

Formats the value using the given formatter.