Module model_judgment 

Structs

InstantiatedModel

Instantiates an existing model into the current model.

MorDecl

Declares a morphism in a model of a double theory.

ObDecl

Declares an object in a model of a double theory.

SpecializeModel

A specialization of a generating object in an instantiated model.

Enums

ModelJudgment

A judgment defining part of a model of a double theory.