Enum fungi_lang::bitype::Ctx
[−]
[src]
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),
}Typing context
Variants
EmptyDef(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
Methods
impl Ctx[src]
pub fn def(&self, v: Var, t: Term) -> Ctx[src]
define a term
pub fn var(&self, v: Var, t: Type) -> Ctx[src]
bind a var and type
pub fn ivar(&self, v: Var, s: Sort) -> Ctx[src]
bind a index var and sort
pub fn tvar(&self, v: Var, k: Kind) -> Ctx[src]
bind a type var and kind
pub fn equiv(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> Ctx[src]
assume an index equivalence
pub fn apart(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> Ctx[src]
assume an index apartness
pub fn prop(&self, p: Prop) -> Ctx[src]
assume a proposition is true
pub fn append(&self, other: &Ctx) -> Ctx[src]
pub fn append_rec(&self, other: &Ctx) -> Rc<Ctx>[src]
impl Ctx[src]
pub fn rest(&self) -> Option<CtxRec>[src]
pub fn lookup_var(&self, x: &Var) -> Option<Type>[src]
pub fn lookup_ivar(&self, x: &Var) -> Option<Sort>[src]
pub fn lookup_tvar(&self, x: &Var) -> Option<Kind>[src]
pub fn lookup_type_def(&self, x: &Var) -> Option<Type>[src]
pub fn lookup_idxtm_def(&self, x: &Var) -> Option<IdxTm>[src]
pub fn find_defs_for_idxtm_var(&self, x: &Var) -> Option<IdxTm>[src]
Trait Implementations
impl Clone for Ctx[src]
fn clone(&self) -> Ctx[src]
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)1.0.0[src]
Performs copy-assignment from source. Read more
impl Debug for Ctx[src]
fn fmt(&self, __arg_0: &mut Formatter) -> Result[src]
Formats the value using the given formatter. Read more
impl Eq for Ctx[src]
impl PartialEq for Ctx[src]
fn eq(&self, __arg_0: &Ctx) -> bool[src]
This method tests for self and other values to be equal, and is used by ==. Read more
fn ne(&self, __arg_0: &Ctx) -> bool[src]
This method tests for !=.