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