Enum nar::check::pats::block::Stuck

pub enum Stuck {
    OnMeta(MI),
    OnElim(Elim),
    UnderApplied,
    AbsurdMatch,
    MissingClauses,
    NotBlocked,
}

A modified version of this thing in Agda.

Variants

OnMeta(MI)

Blocked by meta.

OnElim(Elim)

The Elim is neutral and blocks a pattern match.

UnderApplied

Not enough arguments were supplied to complete the matching.

AbsurdMatch

We matched an absurd clause, results in a neutral Def.

MissingClauses

We ran out of clauses, all considered clauses produced an actual mismatch. This can happen when try to reduce a function application, but we are still missing some function clauses. See Agda.TypeChecking.Patterns.Match.

NotBlocked

Reduction was not blocked, we reached a whnf which can be anything, but a stuck Whnf::Redex.

Methods

impl Stuck

pub fn is_meta(&self) -> Option<MI>

Trait Implementations

impl Add<Stuck> for Stuck

type Output = Self

The resulting type after applying the + operator.

fn add(self, rhs: Self) -> Self::Output

Performs the + operation.

impl Clone for Stuck

fn clone(&self) -> Stuck

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Stuck

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

Formats the value using the given formatter.

impl Default for Stuck

fn default() -> Self

Returns the "default value" for a type.

impl Display for Stuck

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

Formats the value using the given formatter.