|
|
|---|
|
|
|
|---|
Fixtype of Syntheto function specifiers.
This is a tagged union type, introduced by fty::deftagsum.
These are the possible specifiers of Syntheto functions. They are associated to function headers (see function-specification).
Function specifications correspond to second-order functions in ACL2 (currently, represented via SOFT macros). Thus, functions in Syntheto can be specified via the equivalents of soft::defun2 and soft::defun-sk2, which are two possible specifiers.
We also allow, for the case of a specification over a single function, a specifier consisting of a boolean expression over the inputs and outputs of the function; this represents an input/output relation, which can be represented as a quantification, but it is such a common kind of specification that it is worth having a specialized construction for it. A particular kind of input/output relation is a pre/post-condition relation: this can be simply realized via an implication, but we might introduce an even more specialized construction in the future.