Module instance_judgment

Module instance_judgment 

Source

Structs§

InstanceEqnDecl
Declares an equation between two terms in an instance.
InstanceGenDecl
Declares a generator of an instance of a model.
InstanceImport
Imports another instance of the codomain model into this instance.

Enums§

InstanceJudgment
A judgment defining part of an instance of a model of a double theory.
InstanceTm
A term in the language of an instance of a model.