Enum nar::syntax::core::ast::Elim

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

Type for eliminations.

Variants

App(Box<Term>)

Proj(String)

Methods

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 Eq for Elim

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

Performs the conversion.

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

fn from(p: CorePat) -> Elim

Performs the conversion.

impl HasMeta for Elim

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

Inline solved metas inside self.

impl PartialEq<Elim> for Elim

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

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

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

This method tests for !=.

impl RedEx<Elim, Term> for Elim

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

Apply a substitution to a redex.

impl StructuralEq for Elim

impl StructuralPartialEq for Elim

impl Unify for Elim

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

Conversion check, maybe can solve metas.