Struct nar::check::rules::clause::eqs::Equation

pub(super) struct Equation {
    pub in_pat: AbsCopat,
    pub inst: Term,
    pub ty: Term,
}

A user pattern and a core term that they should equal after splitting is complete. Agda.

Fields

in_pat: AbsCopat

The pattern causes this problem.

inst: Term

ty: Term

Trait Implementations

impl Clone for Equation

fn clone(&self) -> Equation

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Equation

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

Formats the value using the given formatter.

impl Eq for Equation

impl PartialEq<Equation> for Equation

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

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

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

This method tests for !=.

impl PatCommon for Equation

fn is_split(&self) -> bool

Whether the pattern is a splitting pattern or not.

fn is_solved(&self) -> bool

impl RedEx<Equation, Term> for Equation

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

Apply a substitution to a redex.

impl StructuralEq for Equation

impl StructuralPartialEq for Equation