Enum Pattern 

pub enum Pattern {
    Wildcard,
    Var(String),
    Ctor {
        name: String,
        args: Vec<Pattern>,
    },
    Numeral(u64),
}

A surface pattern, exactly as a When clause spells it.

Variants

Wildcard

_ — matches anything, binds nothing.

Var(String)

k — matches anything, binds the name to the whole matched value.

Ctor

Succ (Succ k) — a constructor applied to one sub-pattern per VALUE field.

Fields

name: String

args: Vec<Pattern>

Numeral(u64)

0, 2, 17 — a NUMERAL, which is the unary spelling of that number in the inductive the column has. Lean’s | 0 => … | 1 => … (Lean/Meta/Match/Match.lean:629 expandNatValuePattern, reached through isNatValueTransition at :171) expands a Nat literal pattern into Nat.zero/Nat.succ applications before the matrix ever sees it, and so does this compiler — see peano_shape, which derives the pair from the declaration rather than hard-coding Nat, so a user’s own unary numeral type works too.

Implementations

impl Pattern

pub fn binders(&self) -> Vec<String>

Every name this pattern binds, left to right.

pub fn render(&self) -> String

How this pattern reads back, for a diagnostic.

Trait Implementations

impl Clone for Pattern

fn clone(&self) -> Pattern

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Pattern

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

Formats the value using the given formatter.

impl PartialEq for Pattern

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

impl StructuralPartialEq for Pattern