Module val 

Values for types and terms.

See crate::tt for what this means.

Structs

BaseTmV

Values for terms, dereferences to BaseTmV_.

BaseTyV

Value for total types, dereferences to BaseTyV_.

FiberTmV

Values for fiber terms, dereferences to FiberTmV_.

FiberTyV

Values for fiber types, dereferences to FiberTyV_.

RecordV

The content of a record type value.

TmN

Neutrals for terms, dereferences to TmN_.

Enums

BaseTmV_

Inner enum for BaseTmV.

BaseTyV_

Inner enum for BaseTyV.

FiberTmV_

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

FiberTyV_

Inner enum for FiberTyV; value counterpart of super::stx::FiberTyS_.

TmN_

Inner enum for TmN.

Functions

merge_specializations

Merge new specializations with old specializations.

Type Aliases

Env

A way of resolving BwdIdx found in BaseTmS_::Var to values.

FiberEnv

The fiber environment: resolves BwdIdx found in super::stx::FiberTmS_::Var to fiber-term values. Separate from Env, the base environment.