Enum Elim

pub enum Elim {
    App(Box<Term>),
    Proj(String),
}

Type for eliminations.

Variants

App(Box<Term>)

Proj(String)

Implementations

impl Elim

pub fn app(term: Term) -> Self

pub fn is_proj(&self) -> bool

pub fn into_app(self) -> Term

pub fn try_into_app(self) -> Result<Term, String>

Trait Implementations

impl Clone for Elim

fn clone(&self) -> Elim

Returns a copy of the value.

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

Performs copy-assignment from source.

impl DeBruijn for Elim

fn dbi_view(&self) -> Option<DBI>

Agda.

fn from_dbi(dbi: DBI) -> Self

Agda.

impl Debug for Elim

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for Elim

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl FoldVal for Elim

fn try_fold_val<E, R>( &self, init: R, f: impl Fn(R, &Val) -> Result<R, E> + Copy, ) -> Result<R, E>

impl From<Copat<DBI, Term>> for Elim

fn from(p: CoreCopat) -> Elim

Converts to this type from the input type.

impl From<Pat<DBI, Term>> for Elim

fn from(p: CorePat) -> Elim

Converts to this type from the input type.

impl HasMeta for Elim

fn inline_meta(self, tcs: TCS) -> TCMS<Self>

Inline solved metas inside self.

impl PartialEq for Elim

fn eq(&self, other: &Elim) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl RedEx for Elim

fn reduce_dbi(self, subst: Rc<Subst>) -> Elim

Apply a substitution to a redex.

impl Unify for Elim

fn unify(tcs: TCS, left: &Self, right: &Self) -> TCM

Conversion check, maybe can solve metas.

impl Eq for Elim

impl StructuralPartialEq for Elim