Enum FiberTmS_ 

pub enum FiberTmS_ {
    Var(BwdIdx, VarName, LabelSegment),
    Proj(FiberTmS, FieldName, LabelSegment),
    List(Vec<FiberTmS>),
    ObApp(VarName, FiberTmS),
    OverApp(Vec<(FieldName, LabelSegment)>, BaseTmS, FiberTmS),
    Meta(MetaVar),
}

Inner enum for FiberTmS: a term of a fiber type, i.e. an element of an instance.

Fiber terms reference the elaborator’s fiber scope (generators and sub-instance imports), which is separate from the base context; see crate::tt::context::Context. They are all neutral — there is no fiber introduction form yet (mapping out of an instance by a record literal is future work), so a fiber term is always a variable, a projection, or a codomain-morphism application.

Variants

Var(BwdIdx, VarName, LabelSegment)

A fiber-context variable: a generator or a sub-instance import. Backward index into the fiber environment.

Proj(FiberTmS, FieldName, LabelSegment)

Projection of a generator out of a sub-instance import, e.g. we.e.

List(Vec<FiberTmS>)

A fiber list literal [a, b, ...] (possibly empty). Its fiber type is Over([A, B, ...]) where each x_i : Over(A_i). Mirrors base BaseTmS_::List; used to supply the (modal) list argument of a multi-ary morphism, e.g. op[x, x].

ObApp(VarName, FiberTmS)

Application of a theory object-operation to a fiber element, e.g. @tensor [a, b]. Mirrors base BaseTmS_::ObApp; its fiber type is Over(@op ...) over the operation applied to the argument’s base object.

OverApp(Vec<(FieldName, LabelSegment)>, BaseTmS, FiberTmS)

Application of a codomain morphism to a fiber element. Arguments, in order: the path to the morphism in the codomain (a single segment like src, or a nested one like Add.op for a morphism of a sub-model), the codomain object it lands at (a base object term, stored so the result fiber type is recoverable without re-deriving it), and the fiber-typed argument (e.g. the elaboration of we.e, or a fiber list [x, x] for a multi-ary morphism).

Example: in src(we.e) := v1, the LHS elaborates to OverApp([src], self.V, Proj(Var(we), e, e)) of fiber type Over(self.V).

Meta(MetaVar)

A metavar (elaboration-error placeholder).