Enum AgdaPattern 

pub enum AgdaPattern {
    Var(String),
    Con(String, Vec<AgdaPattern>),
    Wildcard,
    Num(i64),
    Dot(Box<AgdaPattern>),
    Absurd,
    As(String, Box<AgdaPattern>),
    Implicit(Box<AgdaPattern>),
}

A pattern in an Agda function definition clause.

Variants

Var(String)

Named variable pattern: n

Con(String, Vec<AgdaPattern>)

Constructor pattern: (ctor p1 p2) or ctor (nullary)

Wildcard

Wildcard pattern: _

Num(i64)

Literal number: 0, 42

Dot(Box<AgdaPattern>)

Dot pattern (inaccessible): .t

Absurd

Absurd pattern: ()

As(String, Box<AgdaPattern>)

As-pattern: n@p

Implicit(Box<AgdaPattern>)

Implicit argument pattern: {p}

Trait Implementations

impl Clone for AgdaPattern

fn clone(&self) -> AgdaPattern

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AgdaPattern

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

Formats the value using the given formatter.

impl Display for AgdaPattern

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

Formats the value using the given formatter.

impl PartialEq for AgdaPattern

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