|
|
|---|
|
|
|
|---|
Fixtype of Syntheto function definers.
This is a tagged union type, introduced by fty::deftagsum.
These are the possible definers of Syntheto functions. They are associated to function headers (see function-definition.
The possible definers are a regular one consisting of an expression that calculates the outputs from the inputs (this corresponds to a defun in ACL2), and a quantified one consisting of a universal or existential quantifier over a list of variables with a boolean expression as the matrix (this corresponds to a defun-sk in ACL2). The regular function definer also has an optional measure expression, which may be present only if the function is recursive.