pub struct BaseTmV(/* private fields */);Expand description
Values for terms, dereferences to BaseTmV_.
Implementations§
Source§impl BaseTmV
impl BaseTmV
Sourcepub fn app(name: VarName, x: BaseTmV) -> Self
pub fn app(name: VarName, x: BaseTmV) -> Self
Smart constructor for BaseTmV, BaseTmV_::App case.
Sourcepub fn empty_cons() -> Self
pub fn empty_cons() -> Self
The empty record value [] — the unique element of the empty
record type. Also serves as the (proof-irrelevant) canonical
inhabitant of Id types under eta.
Sourcepub fn id(x: BaseTmV) -> Self
pub fn id(x: BaseTmV) -> Self
Smart constructor for BaseTmV, BaseTmV_::Id case.
Sourcepub fn tab(mor: BaseTmV) -> Self
pub fn tab(mor: BaseTmV) -> Self
Smart constructor for BaseTmV, BaseTmV_::Tab case.
Sourcepub fn compose(f: BaseTmV, g: BaseTmV) -> Self
pub fn compose(f: BaseTmV, g: BaseTmV) -> Self
Smart constructor for BaseTmV, BaseTmV_::Compose case.
Sourcepub fn meta(mv: MetaVar) -> Self
pub fn meta(mv: MetaVar) -> Self
Smart constructor for BaseTmV, BaseTmV_::Meta case.
Sourcepub fn unwrap_neu(&self) -> TmN
pub fn unwrap_neu(&self) -> TmN
Unwraps a neutral term, or panics.
Trait Implementations§
Auto Trait Implementations§
impl Freeze for BaseTmV
impl RefUnwindSafe for BaseTmV
impl !Send for BaseTmV
impl !Sync for BaseTmV
impl Unpin for BaseTmV
impl UnwindSafe for BaseTmV
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,
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
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<T> Pointable for T
impl<T> Pointable for T
§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.