* This commit extends support for the builtin attribute to user-defined types.
It also adds two new attributes. The builtindecl attribute allows the user
to specify their own SMT-LIB type declaration for a user-defined type.
The dependson attribute is used to indicate when a datatype depends on another
datatype when Boogie cannot figure this out itself (which may happen if
builtin's are used).
Examples of how to use these attributes are in Test/sequence.
* fixup! This commit extends support for the builtin attribute to user-defined types. It also adds two new attributes. The builtindecl attribute allows the user to specify their own SMT-LIB type declaration for a user-defined type. The dependson attribute is used to indicate when a datatype depends on another datatype when Boogie cannot figure this out itself (which may happen if builtin's are used). Examples of how to use these attributes are in Test/sequence.
* fixup! This commit extends support for the builtin attribute to user-defined types. It also adds two new attributes. The builtindecl attribute allows the user to specify their own SMT-LIB type declaration for a user-defined type. The dependson attribute is used to indicate when a datatype depends on another datatype when Boogie cannot figure this out itself (which may happen if builtin's are used). Examples of how to use these attributes are in Test/sequence.
* fixup! This commit extends support for the builtin attribute to user-defined types. It also adds two new attributes. The builtindecl attribute allows the user to specify their own SMT-LIB type declaration for a user-defined type. The dependson attribute is used to indicate when a datatype depends on another datatype when Boogie cannot figure this out itself (which may happen if builtin's are used). Examples of how to use these attributes are in Test/sequence.