Enum minitt::syntax::GenericTelescope

pub enum GenericTelescope<Value: Clone> {
    Nil,
    UpDec(Rc<Self>, Declaration),
    UpVar(Rc<Self>, Pattern, Value),
}

Generic definition for two kinds of telescopes.
Value can be specialized with Value or NormalExpression.

Implementing Eq because of NormalExpression

Variants

Nil

Empty telescope

UpDec(Rc<Self>, Declaration)

In Mini-TT, checked declarations are put here. However, it's not possible to store a recursive declaration as an Expression (which is a member of Declaration) here.

The problem is quite complicated and can be reproduced by checking out 0.1.5 revision and type-check this code:

rec nat : U = sum { Zero 1 | Suc nat };
-- Inductive definition of nat

let one : nat = Zero 0;
let two : nat = Suc one;
-- Unresolved reference

UpVar(Rc<Self>, Pattern, Value)

Usually a local variable, introduced in your telescope

Trait Implementations

impl<Value: PartialEq + Clone> PartialEq<GenericTelescope<Value>> for GenericTelescope<Value>

fn eq(&self, other: &GenericTelescope<Value>) -> bool

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

fn ne(&self, other: &GenericTelescope<Value>) -> bool

This method tests for !=.

impl<Value: Clone + Clone> Clone for GenericTelescope<Value>

fn clone(&self) -> GenericTelescope<Value>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Value: Eq + Clone> Eq for GenericTelescope<Value>

impl<Value: Clone + Display> Display for GenericTelescope<Value>

Actually it's for NeutralTelescope

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

Formats the value using the given formatter.

impl<Value: Debug + Clone> Debug for GenericTelescope<Value>

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

Formats the value using the given formatter.