Enum FiberTmV_ 

pub enum FiberTmV_ {
    Var(FwdIdx, VarName, LabelSegment),
    Proj(FiberTmV, FieldName, LabelSegment),
    List(Vec<FiberTmV>),
    ObApp(VarName, FiberTmV),
    OverApp(Vec<(FieldName, LabelSegment)>, BaseTmV, FiberTmV),
    Meta(MetaVar),
}

Inner enum for FiberTmV; value counterpart of super::stx::FiberTmS_.

Every fiber term is neutral, so — unlike BaseTmV_ — there is no closure/neutral split and no stored type for eta. Variables carry a forward index into the fiber environment.

Variants

Var(FwdIdx, VarName, LabelSegment)

A fiber-context variable (generator or sub-instance import).

Proj(FiberTmV, FieldName, LabelSegment)

Projection of a generator out of a sub-instance import (we.e).

List(Vec<FiberTmV>)

A fiber list literal. See super::stx::FiberTmS_::List.

ObApp(VarName, FiberTmV)

A theory object-operation applied to a fiber element. See super::stx::FiberTmS_::ObApp.

OverApp(Vec<(FieldName, LabelSegment)>, BaseTmV, FiberTmV)

Application of a codomain morphism (identified by its path) to a fiber element; the second field is the codomain object it lands at. See super::stx::FiberTmS_::OverApp.

Meta(MetaVar)

A metavariable.