Enum minitt::ast::Expression

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

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

Variants

Unit

0

One

1

Type(u32)

Type

Void

Empty file

Var(String)

bla

Sum(Branch)

Sum { Bla x }

Split(Branch)

split { Bla x => y }

Pi(Typed, Box<Self>)

\Pi a: b. c

Sigma(Typed, Box<Self>)

\Sigma a: b. c

Lambda(Pattern, Option<AnonymousValue>, Box<Self>)

\lambda a. c, the optional value is the type of the argument.
This cannot be specified during parsing because it's used for generated intermediate values during type-checking.

First(Box<Self>)

bla.1

Second(Box<Self>)

bla.2

Application(Box<Self>, Box<Self>)

f a

Pair(Box<Self>, Box<Self>)

a, b

Constructor(String, Box<Self>)

Cons a

Constant(Pattern, Box<Self>, Box<Self>)

const bla, this is an extension: a declaration whose type-signature is inferred. This is very similar to a Declaration.

Declaration(Box<Declaration>, Box<Self>)

let bla or rec bla

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 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 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.