Struct ErasureContext 

pub struct ErasureContext { /* private fields */ }

An erasure context tracking which variables are types vs terms.

Implementations

impl ErasureContext

pub fn new() -> Self

Create an empty context.

pub fn push(&mut self, is_type: bool)

Push a variable; is_type indicates whether it should be erased.

pub fn pop(&mut self)

Pop the last variable.

pub fn is_type_at(&self, i: u32) -> bool

Return whether the variable at De Bruijn index i is a type.

pub fn depth(&self) -> usize

Return the current depth.

Trait Implementations

impl Default for ErasureContext

fn default() -> Self

Returns the “default value” for a type.