pub struct TyV(/* private fields */);Expand description
Value for total types, dereferences to TyV_.
Implementations§
Source§impl TyV
impl TyV
Sourcepub fn object(object_type: ObjectType) -> Self
pub fn object(object_type: ObjectType) -> Self
Smart constructor for TyV, TyV_::Object case.
Sourcepub fn morphism(morphism_type: MorphismType, dom: TmV, cod: TmV) -> Self
pub fn morphism(morphism_type: MorphismType, dom: TmV, cod: TmV) -> Self
Smart constructor for TyV, TyV_::Morphism case.
Sourcepub fn record(record_v: RecordV) -> Self
pub fn record(record_v: RecordV) -> Self
Smart constructor for TyV, TyV_::Record case.
Sourcepub fn specialize(&self, specializations: &Dtry<TyV>) -> Self
pub fn specialize(&self, specializations: &Dtry<TyV>) -> Self
Compute the specialization of self by specializations.
Specialization is the process of assigning subtypes to the fields of a (possibly nested) record.
There are some subtle points around how multiple specializations compose that we have to think about.
Consider the following:
type r1 = [ A : Type, B : Type, a : A ]
type r2 = [ x : r1, y : x.B ]
type r3 = r2 & [ .x : r1 & [ .A : (= Int) ] ] & [ .x.B : (= Bool) ]
type r3' = r2 & [ .x : r1 & [ .A : (= Int), .B : (= Bool) ] ]
type r3'' = r2 & [ .x.A : (= Int), .x.B : (= Bool) ]r3 and r3’ should be represented in the same way, and r3, r3’ and r3’’ should all be equivalent.
Sourcepub fn add_specialization(
&self,
path: &[(FieldName, LabelSegment)],
ty: TyV,
) -> Self
pub fn add_specialization( &self, path: &[(FieldName, LabelSegment)], ty: TyV, ) -> Self
Specializes the field at path to ty
Precondition: assumes that this produces a subtype.
Sourcepub fn unit() -> Self
pub fn unit() -> Self
Smart constructor for TyV, TyV_::Unit case.
Trait Implementations§
Auto Trait Implementations§
impl Freeze for TyV
impl RefUnwindSafe for TyV
impl !Send for TyV
impl !Sync for TyV
impl Unpin for TyV
impl UnwindSafe for TyV
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.