Struct minitt::check::tcm::TCS

pub struct TCS<'a> {
    pub gamma: Gamma<'a>,
    pub context: Telescope,
}

Type-Checking State , not "Theoretical Computer Science".
This is not present in Mini-TT.

Fields

gamma: Gamma<'a>

context: Telescope

Methods

impl<'a> TCS<'a>

pub fn new(gamma: Gamma<'a>, context: Telescope) -> Self

pub fn context(&self) -> Telescope

Since context is ref-counted, it's gonna be cheap to clone.

pub fn update(
    self,
    pattern: Pattern,
    type_val: Value,
    body: Value
) -> TCM<TCS<'a>>

Trait Implementations

impl<'a> Default for TCS<'a>

fn default() -> Self

Returns the "default value" for a type.

impl<'a> Debug for TCS<'a>

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

Formats the value using the given formatter.