Struct Telescope 

pub struct Telescope {
    pub binders: Vec<(Name, Expr)>,
}

A telescope is a sequence of (name, type) binders, where later types may depend on earlier names.

This is the standard way to represent the argument list of a function type (x₁ : T₁) → (x₂ : T₂[x₁]) → … → B.

Fields

binders: Vec<(Name, Expr)>

Binders in order from outermost to innermost.

Implementations

impl Telescope

pub fn new() -> Self

Create an empty telescope.

pub fn push(&mut self, name: Name, ty: Expr)

Add a binder to the end of the telescope.

pub fn len(&self) -> usize

Return the length of the telescope.

pub fn is_empty(&self) -> bool

Check if the telescope is empty.

pub fn from_pi(expr: &Expr) -> (Self, Expr)

Extract the telescope from a Pi type.

telescope_of(Pi(x: A, Pi(y: B, C))) returns [(x, A), (y, B)] and body C.

pub fn to_pi(&self, body: Expr) -> Expr

Reconstruct the Pi type from this telescope and a body.

pub fn to_lam(&self, body: Expr) -> Expr

Reconstruct a Lambda from this telescope and a body.

pub fn instantiate(&self, args: &[Expr]) -> Vec<Expr>

Instantiate the telescope with a list of expressions.

Returns the types with de Bruijn indices resolved.

Trait Implementations

impl Clone for Telescope

fn clone(&self) -> Telescope

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Telescope

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

Formats the value using the given formatter.

impl Default for Telescope

fn default() -> Telescope

Returns the “default value” for a type.