Enum fungi_lang::decide::RelCtx
source · pub enum RelCtx {
Empty,
Ctx(Ctx),
NVarEquiv(RelCtxRec, Var, Var, Sort),
NVarApart(RelCtxRec, Var, Var, Sort),
IVarEquiv(RelCtxRec, Var, Var, Sort),
IVarApart(RelCtxRec, Var, Var, Sort),
PropTrue(RelCtxRec, Prop),
TVarRelated(RelCtxRec, Var, Var),
}
Expand description
Relational typing context: Relates pairs of variables, terms, etc
Variants
Empty
Basecase 1: empty context
Ctx(Ctx)
Basecase 2: Non-relational typing context
NVarEquiv(RelCtxRec, Var, Var, Sort)
Assume a name variable equivalence, at a common sort
NVarApart(RelCtxRec, Var, Var, Sort)
Assume a name variable apartness, at a common sort
IVarEquiv(RelCtxRec, Var, Var, Sort)
Assume an index variable equivalence, at a common sort
IVarApart(RelCtxRec, Var, Var, Sort)
Assume an index variable apartness, at a common sort
PropTrue(RelCtxRec, Prop)
Assume a proposition is true
TVarRelated(RelCtxRec, Var, Var)
Type variables are related: TODO: Kinds?
Implementations
sourceimpl RelCtx
impl RelCtx
pub fn prop_true(&self, p: Prop) -> Self
pub fn add_tvars(&self, a: Var, b: Var) -> Self
pub fn add_ivars(&self, a: Var, b: Var, g: Sort) -> Self
pub fn ivar(&self, a: Var, b: Var, g: Sort) -> Self
pub fn nt_eq(&self, n1: &Var, n2: &Var, g: &Sort) -> Self
pub fn lookup_type_def(&self, x: &Var) -> Option<Type>
pub fn rest(&self) -> Option<RelCtxRec>
pub fn lookup_tvars(&self, x1: &Var, x2: &Var) -> bool
pub fn lookup_nvareq(&self, x1: &Var, x2: &Var, g: &Sort) -> bool
pub fn lookup_ivareq(&self, x1: &Var, x2: &Var, g: &Sort) -> bool
pub fn lookup_nvarapart(&self, x1: &Var, x2: &Var, g: &Sort) -> bool
pub fn lookup_bitype_ctx(&self) -> Ctx
pub fn lookup_ivarapart(&self, x1: &Var, x2: &Var, g: &Sort) -> bool
Trait Implementations
impl Eq for RelCtx
impl StructuralEq for RelCtx
impl StructuralPartialEq for RelCtx
Auto Trait Implementations
impl RefUnwindSafe for RelCtx
impl !Send for RelCtx
impl !Sync for RelCtx
impl Unpin for RelCtx
impl UnwindSafe for RelCtx
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