Enum nar::syntax::pat::Copat

pub enum Copat<Ix, Term> {
    App(Pat<Ix, Term>),
    Proj(String),
}

Copatterns. The Ix is the representation of variable abstraction, like UID in abstract or DBI in core.

Variants

App(Pat<Ix, Term>)

Application copatterns.

Proj(String)

Projection copatterns.

Methods

impl<Ix, Term> Copat<Ix, Term>

pub fn absurd() -> Self

pub fn reflexivity() -> Self

pub fn var(ix: Ix) -> Self

pub fn term(term: Term) -> Self

pub fn cons(is_forced: bool, cons: ConHead, pats: Vec<Pat<Ix, Term>>) -> Self

pub fn is_proj(&self) -> bool

pub fn map_app<Ix2, Term2>(
    self,
    f: impl FnOnce(Pat<Ix, Term>) -> Pat<Ix2, Term2>
) -> Copat<Ix2, Term2>

impl<Term> Copat<UID, Term>

pub fn fresh_var() -> Self

Trait Implementations

impl<Ix: Clone, Term: Clone> Clone for Copat<Ix, Term>

fn clone(&self) -> Copat<Ix, Term>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Ix: Debug, Term: Debug> Debug for Copat<Ix, Term>

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

Formats the value using the given formatter.

impl<Ix: Eq, Term: Eq> Eq for Copat<Ix, Term>

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

fn from(p: CoreCopat) -> Elim

Performs the conversion.

impl<Ix: PartialEq, Term: PartialEq> PartialEq<Copat<Ix, Term>> for Copat<Ix, Term>

fn eq(&self, other: &Copat<Ix, Term>) -> bool

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

fn ne(&self, other: &Copat<Ix, Term>) -> bool

This method tests for !=.

impl<Ix, Term> PatCommon for Copat<Ix, Term>

fn is_split(&self) -> bool

Whether the pattern is a splitting pattern or not.

fn is_solved(&self) -> bool

impl<Ix, R, T: RedEx<R>> RedEx<Copat<Ix, R>, Term> for Copat<Ix, T>

fn reduce_dbi(self, subst: Rc<Subst>) -> Copat<Ix, R>

Apply a substitution to a redex.

impl<Ix, Term> StructuralEq for Copat<Ix, Term>

impl<Ix, Term> StructuralPartialEq for Copat<Ix, Term>

impl TryFrom<Copat<DBI, Term>> for Term

type Error = String

The type returned in the event of a conversion error.

fn try_from(p: CoreCopat) -> Result<Term, String>

Performs the conversion.