Enum BaseTyS_ 

pub enum BaseTyS_ {
    TopVar(TopVarName),
    Object(ObType),
    Morphism(MorType, BaseTmS, BaseTmS),
    Record(Row<BaseTyS>),
    Sing(BaseTyS, BaseTmS),
    Id(BaseTyS, BaseTmS, BaseTmS),
    Specialize(BaseTyS, Vec<(Vec<(FieldName, LabelSegment)>, BaseTyS)>),
    Meta(MetaVar),
}

Inner enum for BaseTyS.

Variants

TopVar(TopVarName)

A reference to a top-level declaration.

Object(ObType)

Type constructor for object types.

Example syntax: Entity (top-level constants are bound by the elaborator to various object types).

A term of type Object(ot) represents an object of object type ot.

Morphism(MorType, BaseTmS, BaseTmS)

Type constructor for morphism types.

Example syntax: Attr x a (top-level constants are bound by the elaborator to constructors for morphism types).

A term of type Morphism(mt, dom, cod) represents an morphism of morphism type mt from dom to cod.

Record(Row<BaseTyS>)

Type constructor for record types.

Example syntax: [x : A, y : B].

A term x of type Record(r) represents a record where field f has type eval(env.snoc(eval(env, x)), r.fields1[f]).

Sing(BaseTyS, BaseTmS)

Type constructor for singleton types.

Example syntax: @sing a (assuming a is a term that synthesizes a type).

A term x of type Sing(ty, tm) is a term of ty that is convertible with tm.

Id(BaseTyS, BaseTmS, BaseTmS)

Type constructor for identity types.

Example syntax: a == b (assuming a and b are terms that synthesize the same type).

A term p of type a == b is a proof that a and b are equal.

Specialize(BaseTyS, Vec<(Vec<(FieldName, LabelSegment)>, BaseTyS)>)

Type constructor for specialized types.

Example syntax: A & [ .x : @sing a ].

A term x of type Specialize(ty, d) is a term of ty where additionally for each path p (e.g. .x, .a.b, etc.) in d, x.p is of type d[p].

In order to form this type, it must be the case that d[p] is a subtype of the type of the field at path p.

Meta(MetaVar)

A metavar.

Currently, this is only used for handling elaboration errors, we might add more unification/holes later.