pub enum TmV {
Neu(TmN, TyV),
Cons(Row<TmV>),
Tt,
Opaque,
}Expand description
Values for base terms.
Note that this is not the value for total terms. So evaluating a TmS to
produce a TmV and then quoting back will lose information about anything
morphism-related. See crate::tt for more information.
It turns out that each of the cases for TmV has a single cheaply cloneable
field, so we don’t need to bother making a TmV_.
Variants§
Neu(TmN, TyV)
Neutrals.
We store the type because we need it for eta-expansion.
Cons(Row<TmV>)
Records.
Tt
The unique element of Ty0::Unit.
Opaque
An element of a type that is opaque to conversion checking
Implementations§
Trait Implementations§
Auto Trait Implementations§
impl Freeze for TmV
impl RefUnwindSafe for TmV
impl !Send for TmV
impl !Sync for TmV
impl Unpin for TmV
impl UnwindSafe for TmV
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more§impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
impl<SS, SP> SupersetOf<SS> for SPwhere
SS: SubsetOf<SP>,
§fn to_subset(&self) -> Option<SS>
fn to_subset(&self) -> Option<SS>
The inverse inclusion map: attempts to construct
self from the equivalent element of its
superset. Read more§fn is_in_subset(&self) -> bool
fn is_in_subset(&self) -> bool
Checks if
self is actually part of its subset T (and can be converted to it).§fn to_subset_unchecked(&self) -> SS
fn to_subset_unchecked(&self) -> SS
Use with care! Same as
self.to_subset but without any property checks. Always succeeds.§fn from_subset(element: &SS) -> SP
fn from_subset(element: &SS) -> SP
The inclusion map: converts
self to the equivalent element of its superset.