Struct BaseTyV &nbsp; Copy item path

impl BaseTyV

pub fn object(object_type: ObType) -> Self

Smart constructor for BaseTyV, BaseTyV_::Object case.

pub fn morphism(morphism_type: MorType, dom: BaseTmV, cod: BaseTmV) -> Self

Smart constructor for BaseTyV, BaseTyV_::Morphism case.

pub fn record(record_v: RecordV) -> Self

Smart constructor for BaseTyV, BaseTyV_::Record case.

pub fn sing(ty_v: BaseTyV, tm_v: BaseTmV) -> Self

Smart constructor for BaseTyV, BaseTyV_::Sing case.

pub fn id(ty_v: BaseTyV, tm_v1: BaseTmV, tm_v2: BaseTmV) -> Self

Smart constructor for BaseTyV, BaseTyV_::Id case.

pub fn specialize(&self, specializations: &Dtry<BaseTyV>) -> 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.

pub fn add_specialization( &self, path: &[(FieldName, LabelSegment)], ty: BaseTyV, ) -> Self

Specializes the field at path to ty.

Precondition: assumes that this produces a subtype.

pub fn empty_record() -> Self

The empty record type — the unit type / empty model. Also used as a throwaway type for untyped placeholder binders (whose type is discarded).

pub fn meta(mv: MetaVar) -> Self

Smart constructor for BaseTyV, BaseTyV_::Meta case.

Trait Implementations§

impl Clone for BaseTyV

fn clone(&self) -> BaseTyV

Returns a duplicate of the value. Read more

1.0.0 · Source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more

impl Deref for BaseTyV
where Rc<BaseTyV_>: Deref,

type Target = <Rc<BaseTyV_> as Deref>::Target

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

Auto Trait Implementations§

impl UnwindSafe for BaseTyV

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> DynClone for T
where T: Clone,

fn __clone_box(&self, _: Private) -> *mut ()

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T> Instrument for T

fn instrument(self, span: Span) -> Instrumented<Self>

Instruments this type with the provided [Span], returning an Instrumented wrapper. Read more

fn in_current_span(self) -> Instrumented<Self>

Instruments this type with the current Span, returning an Instrumented wrapper. Read more

impl<T, U> Into for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T> IntoEither for T

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 more

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

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