|
|
|---|
|
|
|
|---|
Fixtype of Syntheto function specifications.
This is a product type introduced by fty::defprod.
This is essentially a second-order predicate over Syntheto functions. A specification defines a set of possible choices for the functions: these are exactly the ones for which the second-order predicate is true. The synthesis process narrows down the set of choices, until a single choice is reached.
Thus, a function specification has a name (of the predicate), function headers (the arguments of the predicate), and a function specifier. The input/output function specifier may be used only if there is a single function.
The specifier may refer to the names of other specifications as if they were nullary Syntheto functions (because the function arguments are implicit). This is how these predicates are handled in ACL2.