Module modelgen 

Generate catlog models from DoubleTT types.

Enums

Model

A model generated by DoubleTT.

ModelInstance

An instance of a model generated by DoubleTT.

NormalizedInstanceTerm

The flat normal form of a single instance term, as produced by normalize_instance_term: a composite model morphism applied to a base of generators. Doctrine-specific because each has its own term type.

Functions

instance_from_def

Generates a ModelInstance from an elaborated Instance declaration.

normalize_instance_term

Normalizes a single already-elaborated fiber term tm (lying over the codomain object over) in the context of the instance inst, returning its flat normal form.