Struct Clause

pub struct Clause {
    pub pat_tele: Tele,
    pub patterns: Vec<CoreCopat>,
    pub body: Option<Term>,
}

Function clauses. Agda.

Fields

pat_tele: Tele

$\Delta$. The types of the pattern variables in dependency order.

patterns: Vec<CoreCopat>

$\Delta \vdash ps$. The de Bruijn indices refer to $\Delta$.

body: Option<Term>

Some(v) if $\Delta \vdash v$, while None if the patterns are absurd.

Implementations

impl Clause

pub fn is_absurd(&self) -> bool

Trait Implementations

impl Clone for Clause

fn clone(&self) -> Clause

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Clause

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

Formats the value using the given formatter.

impl PartialEq for Clause

fn eq(&self, other: &Clause) -> 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 Eq for Clause

impl StructuralPartialEq for Clause