[][src]Enum minitt::ast::GenericTelescope

pub enum GenericTelescope<Value: Clone> {
    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



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:

This example is not tested
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>[src]

impl<Value: Clone + Clone> Clone for GenericTelescope<Value>[src]

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

Performs copy-assignment from source. Read more

impl<Value: Eq + Clone> Eq for GenericTelescope<Value>[src]

impl<Value: Clone + Display> Display for GenericTelescope<Value>[src]

Actually it's for NeutralTelescope

impl<Value: Debug + Clone> Debug for GenericTelescope<Value>[src]

Auto Trait Implementations

impl<Value> !Send for GenericTelescope<Value>

impl<Value> !Sync for GenericTelescope<Value>

Blanket Implementations

impl<T, U> Into for T where
    U: From<T>, 

impl<T> ToOwned for T where
    T: Clone

type Owned = T

impl<T> ToString for T where
    T: Display + ?Sized

impl<T> From for T[src]

impl<T, U> TryFrom for T where
    U: Into<T>, 

type Error = Infallible

The type returned in the event of a conversion error.

impl<T> Borrow for T where
    T: ?Sized

impl<T> BorrowMut for T where
    T: ?Sized

impl<T, U> TryInto for T where
    U: TryFrom<T>, 

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

impl<T> Any for T where
    T: 'static + ?Sized