Enum fungi_lang::bitype::TCtxt

pub enum TCtxt {
    Empty,
    Var(TCtxtRec, Var, Type),
    IVar(TCtxtRec, Var, Sort),
    TVar(TCtxtRec, Var, Kind),
    TCons(TCtxtRec, TypeCons, Kind),
    Equiv(TCtxtRec, IdxTm, IdxTm, Sort),
    Apart(TCtxtRec, IdxTm, IdxTm, Sort),
    PropTrue(TCtxtRec, Prop),
}

Variants

EmptyVar(TCtxtRec, Var, Type)IVar(TCtxtRec, Var, Sort)TVar(TCtxtRec, Var, Kind)TCons(TCtxtRec, TypeCons, Kind)Equiv(TCtxtRec, IdxTm, IdxTm, Sort)Apart(TCtxtRec, IdxTm, IdxTm, Sort)PropTrue(TCtxtRec, Prop)

Methods

impl TCtxt

fn var(&self, v: Var, t: Type) -> TCtxt

bind a var and type

fn ivar(&self, v: Var, s: Sort) -> TCtxt

bind a index var and sort

fn tvar(&self, v: Var, k: Kind) -> TCtxt

bind a type var and kind

fn tcons(&self, d: TypeCons, k: Kind) -> TCtxt

bind a type constructor and kind

fn equiv(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> TCtxt

bind an index equivalence

fn apart(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> TCtxt

bind an index apartness

fn prop(&self, p: Prop) -> TCtxt

bind a true proposition

impl TCtxt

fn lookup_var(&self, x: &Var) -> Option<Type>

fn lookup_ivar(&self, x: &Var) -> Option<Sort>

fn lookup_tvar(&self, x: &Var) -> Option<Kind>

fn lookup_tcons(&self, x: &TypeCons) -> Option<Kind>

fn lookup_equiv(&self, idx1: &IdxTm, idx2: &IdxTm) -> Option<Sort>

fn lookup_apart(&self, idx1: &IdxTm, idx2: &IdxTm) -> Option<Sort>

fn lookup_prop(&self, prop: &Prop) -> bool

Trait Implementations

impl Clone for TCtxt

fn clone(&self) -> TCtxt

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for TCtxt

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

Formats the value using the given formatter.

impl Eq for TCtxt

impl PartialEq for TCtxt

fn eq(&self, __arg_0: &TCtxt) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, __arg_0: &TCtxt) -> bool

This method tests for !=.

impl Hash for TCtxt

fn hash<__H: Hasher>(&self, __arg_0: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].