pub struct FiberTmV(/* private fields */);Expand description
Values for fiber terms, dereferences to FiberTmV_.
Implementations§
Source§impl FiberTmV
impl FiberTmV
Sourcepub fn var(fwd_idx: FwdIdx, var_name: VarName, label: LabelSegment) -> Self
pub fn var(fwd_idx: FwdIdx, var_name: VarName, label: LabelSegment) -> Self
Smart constructor for FiberTmV, FiberTmV_::Var case.
Sourcepub fn proj(tm: FiberTmV, field_name: FieldName, label: LabelSegment) -> Self
pub fn proj(tm: FiberTmV, field_name: FieldName, label: LabelSegment) -> Self
Smart constructor for FiberTmV, FiberTmV_::Proj case.
Sourcepub fn list(elems: Vec<FiberTmV>) -> Self
pub fn list(elems: Vec<FiberTmV>) -> Self
Smart constructor for FiberTmV, FiberTmV_::List case.
Sourcepub fn ob_app(name: VarName, arg: FiberTmV) -> Self
pub fn ob_app(name: VarName, arg: FiberTmV) -> Self
Smart constructor for FiberTmV, FiberTmV_::ObApp case.
Sourcepub fn over_app(
mor: Vec<(FieldName, LabelSegment)>,
cod: BaseTmV,
inner: FiberTmV,
) -> Self
pub fn over_app( mor: Vec<(FieldName, LabelSegment)>, cod: BaseTmV, inner: FiberTmV, ) -> Self
Smart constructor for FiberTmV, FiberTmV_::OverApp case.
Sourcepub fn meta(mv: MetaVar) -> Self
pub fn meta(mv: MetaVar) -> Self
Smart constructor for FiberTmV, FiberTmV_::Meta case.
Trait Implementations§
Auto Trait Implementations§
impl Freeze for FiberTmV
impl RefUnwindSafe for FiberTmV
impl !Send for FiberTmV
impl !Sync for FiberTmV
impl Unpin for FiberTmV
impl UnwindSafe for FiberTmV
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.