Enum TyS_

pub enum TyS_ {
    TopVar(TopVarName),
    Object(ObjectType),
    Morphism(MorphismType, TmS, TmS),
    Record(RecordS),
    Sing(TyS, TmS),
    Specialize(TyS, Vec<(Vec<(FieldName, LabelSegment)>, TyS)>),
    Unit,
}

Inner enum for TyS.

Variants

TopVar(TopVarName)

A reference to a top-level declaration

Object(ObjectType)

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.

The base type for Object(ot) is Ty0::Object(ot).

Morphism(MorphismType, TmS, TmS)

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.

The base type for Morphism(mt, dom, cod) is Ty0::Unit.

Record(RecordS)

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]).

The base type for Record(r) is Ty0::Record(r.fields0).

Sing(TyS, TmS)

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 convertable with tm.

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

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.

Unit

Type constructor for the unit type.

Example syntax: Unit.

All terms of this type are convertable with tt : Unit.