[−][src]Enum voile::syntax::core::ast::Neutral
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.
Lifting self to a higher level.
Down-lifting self to a lower level.
Axi(Axiom)
Postulated value, aka axioms.
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.
Projecting a named element of a record.
Row-polymorphic types.
Record literal, with extension.
Splitting on a neutral term.
Splitting with unknown branches.
Methods
impl Neutral
[src]
pub fn map_axiom(self, f: &mut impl FnMut(Axiom) -> Neutral) -> Self
[src]
fn map_axiom_split(
mapper: &mut impl FnMut(Neutral) -> Val,
split: CaseSplit
) -> CaseSplit
[src]
mapper: &mut impl FnMut(Neutral) -> Val,
split: CaseSplit
) -> CaseSplit
Trait Implementations
impl RedEx<Val> for Neutral
[src]
fn reduce_with_dbi(self, arg: Val, dbi: DBI) -> Val
[src]
fn reduce_with_dbi_borrow(self, arg: &Val, dbi: DBI) -> Val
[src]
impl Clone for Neutral
[src]
impl Eq for Neutral
[src]
fn assert_receiver_is_total_eq(&self)
[src]
impl PartialEq<Neutral> for Neutral
[src]
impl Display for Neutral
[src]
impl Debug for Neutral
[src]
impl StructuralPartialEq for Neutral
[src]
impl StructuralEq for Neutral
[src]
impl LiftEx for Neutral
[src]
Auto Trait Implementations
impl Send for Neutral
impl Sync for Neutral
impl Unpin for Neutral
impl UnwindSafe for Neutral
impl RefUnwindSafe for Neutral
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,