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
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
Methods
impl Ctx
[src]
fn def(&self, v: Var, t: Term) -> Ctx
[src]
define a term
fn var(&self, v: Var, t: Type) -> Ctx
[src]
bind a var and type
fn ivar(&self, v: Var, s: Sort) -> Ctx
[src]
bind a index var and sort
fn tvar(&self, v: Var, k: Kind) -> Ctx
[src]
bind a type var and kind
fn equiv(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> Ctx
[src]
assume an index equivalence
fn apart(&self, i1: IdxTm, i2: IdxTm, s: Sort) -> Ctx
[src]
assume an index apartness
fn prop(&self, p: Prop) -> Ctx
[src]
assume a proposition is true
fn append(&self, other: &Ctx) -> Ctx
[src]
fn append_rec(&self, other: &Ctx) -> Rc<Ctx>
[src]
impl Ctx
[src]
fn rest(&self) -> Option<CtxRec>
[src]
fn lookup_var(&self, x: &Var) -> Option<Type>
[src]
fn lookup_ivar(&self, x: &Var) -> Option<Sort>
[src]
fn lookup_tvar(&self, x: &Var) -> Option<Kind>
[src]
fn lookup_type_def(&self, x: &Var) -> Option<Type>
[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]
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 !=
.