Enum fungi_lang::decide::RelCtx

pub enum RelCtx {
    Empty,
    NVar(RelCtxRec, Var, Var, Sort),
    IVar(RelCtxRec, Var, Var, Sort),
    TVar(RelCtxRec, Var, Var, Kind),
    Equiv(RelCtxRec, IdxTm, IdxTm, Sort),
    Apart(RelCtxRec, IdxTm, IdxTm, Sort),
    PropTrue(RelCtxRec, Prop),
}

Relational typing context: Relates pairs of variables, terms, etc

Variants

EmptyNVar(RelCtxRec, Var, Var, Sort)

Define a name variable's sort

IVar(RelCtxRec, Var, Var, Sort)

Define an index variable's sort

TVar(RelCtxRec, Var, Var, Kind)

Define a type variable's kind

Equiv(RelCtxRec, IdxTm, IdxTm, Sort)

Assume an index term equivalence, at a common sort

Apart(RelCtxRec, IdxTm, IdxTm, Sort)

Assume an index term apartness, at a common sort

PropTrue(RelCtxRec, Prop)

Assume a proposition is true

Trait Implementations

impl Clone for RelCtx

fn clone(&self) -> RelCtx

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RelCtx

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Eq for RelCtx

impl PartialEq for RelCtx

fn eq(&self, __arg_0: &RelCtx) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, __arg_0: &RelCtx) -> bool

This method tests for !=.

impl Hash for RelCtx

fn hash<__H: Hasher>(&self, __arg_0: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].