Module stx

Syntax for types and terms.

See crate::tt for what this means.

Structs

MorphismType

Morphism types are paths of qualified names, see DiscreteDblTheory.

RecordS

Content of record type syntax.

TmS

Syntax for total terms, dereferences to TmS_.

TyS

Syntax for total types, dereferences to TyS_.

Enums

TmS_

Inner enum for TmS.

Ty0

Type in the base type theory.

TyS_

Inner enum for TyS.

Type Aliases

ObjectType

Object types are just qualified names, see DiscreteDblTheory.