cvc4-1.4
|
A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself. More...
#include <datatype.h>
A holder type (used in calls to DatatypeConstructor::addArg()) to allow a Datatype to refer to itself.
Self-typed fields of Datatypes will be properly typed when a Type is created for the Datatype by the ExprManager (which calls Datatype::resolve()).
Definition at line 98 of file datatype.h.