Enum fungi_lang::bitype::Ctx
source · pub enum Ctx {
Empty,
Def(CtxRec, Var, Term),
Var(CtxRec, Var, Type),
IVar(CtxRec, Var, Sort),
TVar(CtxRec, Var, Kind),
Equiv(CtxRec, IdxTm, IdxTm, Sort),
Apart(CtxRec, IdxTm, IdxTm, Sort),
PropTrue(CtxRec, Prop),
}
Expand description
Typing context
Variants
Empty
Def(CtxRec, Var, Term)
Define a type term to be carried in the type context
Var(CtxRec, Var, Type)
Define a value variable’s type
IVar(CtxRec, Var, Sort)
Define a name/index variable’s sort
TVar(CtxRec, Var, Kind)
Define a type variable’s kind
Equiv(CtxRec, IdxTm, IdxTm, Sort)
Assume an index term equivalence, at a common sort
Apart(CtxRec, IdxTm, IdxTm, Sort)
Assume an index term apartness, at a common sort
PropTrue(CtxRec, Prop)
Assume a proposition is true
Implementations
sourceimpl Ctx
impl Ctx
sourceimpl Ctx
impl Ctx
pub fn rest(&self) -> Option<CtxRec>
pub fn lookup_var(&self, x: &Var) -> Option<Type>
pub fn lookup_ivar(&self, x: &Var) -> Option<Sort>
pub fn lookup_tvar(&self, x: &Var) -> Option<Kind>
pub fn lookup_type_def(&self, x: &Var) -> Option<Type>
pub fn lookup_idxtm_def(&self, x: &Var) -> Option<IdxTm>
pub fn lookup_nmtm_def(&self, x: &Var) -> Option<NameTm>
pub fn find_defs_for_idxtm_var(&self, x: &Var) -> Option<IdxTm>
pub fn only_defs(&self) -> Ctx
Trait Implementations
impl Eq for Ctx
impl StructuralEq for Ctx
impl StructuralPartialEq for Ctx
Auto Trait Implementations
impl RefUnwindSafe for Ctx
impl !Send for Ctx
impl !Sync for Ctx
impl Unpin for Ctx
impl UnwindSafe for Ctx
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more