Struct TelescopeExt2 

pub struct TelescopeExt2 {
    pub binders: Vec<BinderExtExt2>,
}

A telescope: a sequence of binders.

Fields

binders: Vec<BinderExtExt2>

The binders in order

Implementations

impl TelescopeExt2

pub fn new() -> Self

Create an empty telescope.

pub fn push(&mut self, b: BinderExtExt2)

Add a binder.

pub fn len(&self) -> usize

Returns the number of binders.

pub fn is_empty(&self) -> bool

Returns true if empty.

pub fn format(&self) -> String

Format as a space-separated list of binder strings.

Trait Implementations

impl Clone for TelescopeExt2

fn clone(&self) -> TelescopeExt2

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TelescopeExt2

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

Formats the value using the given formatter.

impl Default for TelescopeExt2

fn default() -> TelescopeExt2

Returns the “default value” for a type.