Enum voile::syntax::core::ast::Neutral

pub enum Neutral {
    Var(DBI),
    Ref(DBI),
    Lift(u32, Box<Self>),
    Axi(Axiom),
    App(Box<Self>, Box<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(DBI)

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

Lift(u32, Box<Self>)

Lifting self to a higher/lower level.

Axi(Axiom)

Postulated value, aka axioms.

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

Function application.

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<F: Fn(Axiom) -> Self + Copy>(self, f: F) -> 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.

impl AxiomEx for Neutral

fn generated_to_var(self) -> Self

fn unimplemented_to_glob(self) -> Self

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 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 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 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.