Enum BaseTmS_ 

pub enum BaseTmS_ {
    TopApp(TopVarName, Vec<BaseTmS>),
    Var(BwdIdx, VarName, LabelSegment),
    Cons(Row<BaseTmS>),
    Proj(BaseTmS, FieldName, LabelSegment),
    Id(BaseTmS),
    Tab(BaseTmS),
    Compose(BaseTmS, BaseTmS),
    ObApp(VarName, BaseTmS),
    List(Vec<BaseTmS>),
    Meta(MetaVar),
}

Inner enum for BaseTmS.

Variants

TopApp(TopVarName, Vec<BaseTmS>)

An application of a top-level term judgment to arguments.

A closed term (a nullary def, e.g. tt : Unit) is the empty-argument case TopApp(name, []).

Var(BwdIdx, VarName, LabelSegment)

Variable syntax.

We use a backward index, as when we evaluate we store the environment in a [bwd::Bwd], and this indexes into that.

Cons(Row<BaseTmS>)

Record introduction.

Proj(BaseTmS, FieldName, LabelSegment)

Record elimination.

Id(BaseTmS)

Identity morphism at an object.

Tab(BaseTmS)

Tabulation of a morphism.

Compose(BaseTmS, BaseTmS)

Composite of two morphisms.

ObApp(VarName, BaseTmS)

Application of an object operation in the theory.

List(Vec<BaseTmS>)

List of objects.

Meta(MetaVar)

A metavar.

This only appears when we have an error in elaboration.