Enum voile::syntax::core::Neutral

pub enum Neutral {
    Var(DBI),
    Ref(GI),
    Meta(MI),
    Lift(u32, Box<Self>),
    Axi(Axiom),
    App(Box<Self>, Vec<Val>),
    Fst(Box<Self>),
    Snd(Box<Self>),
}

Irreducible because of the presence of generated value.

Variants

Var(DBI)

Local variable, referred by de-bruijn index.

Ref(GI)

Global variable, referred by index. Needed for recursive definitions.

Meta(MI)

Meta variable reference.

Lift(u32, Box<Self>)

Lifting self to a higher/lower level.

Axi(Axiom)

Postulated value, aka axioms.

App(Box<Self>, Vec<Val>)

Function application, with all arguments collected (so we have easy access to application arguments).
This is convenient for meta resolution and termination check.

The "arguments" is supposed to be non-empty.

Fst(Box<Self>)

Projecting the first element of a pair.

Snd(Box<Self>)

Projecting the second element of a pair.

Methods

impl Neutral

pub fn map_axiom(self, f: &mut impl FnMut(Axiom) -> Neutral) -> Self

Trait Implementations

impl RedEx for Neutral

fn reduce_with_dbi(self, arg: Val, dbi: DBI) -> Val

This is primarily a private implementation-related API. Use at your own risk.

fn reduce_with_dbi_borrow(self, arg: &Val, dbi: DBI) -> Val

When the argument is not likely to be used, prefer this over reduce_with_dbi.

impl LiftEx for Neutral

fn lift(self, levels: u32) -> Self

Lift the level of self.

fn calc_level(&self) -> Option<Level>

Internal API, for code sharing only.

fn level(&self) -> Level

Calculate the level of self, like a normal value will have level 0, a type expression will have level 1 (or higher).

impl PartialEq<Neutral> for Neutral

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

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

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

This method tests for !=.

impl Eq for Neutral

fn assert_receiver_is_total_eq(&self)

impl Clone for Neutral

fn clone(&self) -> Neutral

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Neutral

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

Formats the value using the given formatter.

impl Display for Neutral

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

Formats the value using the given formatter.