Enum minitt::check::read_back::NormalExpression

pub enum NormalExpression {
    Lambda(u32, Box<Self>),
    Pair(Box<Self>, Box<Self>),
    Unit,
    One,
    Type(Level),
    Pi(Box<Self>, u32, Box<Self>),
    Sigma(Box<Self>, u32, Box<Self>),
    Constructor(String, Box<Self>),
    Split(NormalCaseTree),
    Sum(NormalCaseTree),
    Neutral(NormalNeutral),
}

NExp in Mini-TT, normal form expressions.
Deriving Eq so we can do comparison.

$E ::=$

Variants

Lambda(u32, Box<Self>)

$\lambda \textsf{x}_i\ .\ E$

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

$E_1, E_2$

Unit

$0$

One

$\textbf{1}$

Type(Level)

$\textsf{U}$

Pi(Box<Self>, u32, Box<Self>)

$\Pi \textsf{x}_i:E_1.E_2$

Sigma(Box<Self>, u32, Box<Self>)

$\Sigma \textsf{x}_i:E_1.E_2$

Constructor(String, Box<Self>)

$c\ E$

Split(NormalCaseTree)

$\textsf{fun}\lang S,\alpha \rang$

Sum(NormalCaseTree)

$\textsf{Sum}\lang S,\alpha \rang$

Neutral(NormalNeutral)

$[K]$

Trait Implementations

impl Eq for NormalExpression

fn assert_receiver_is_total_eq(&self)

impl Clone for NormalExpression

fn clone(&self) -> NormalExpression

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq<NormalExpression> for NormalExpression

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

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

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

This method tests for !=.

impl Debug for NormalExpression

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

Formats the value using the given formatter.

impl Display for NormalExpression

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

Formats the value using the given formatter.