Fixtype of type results.
This is a tagged union type, introduced by fty::deftagsum.
These are the possible results of checking that an expression satisfies the constraints of the static semantics. If the check fails, we return an error, which may contain information, which we do not constraint to be a fixtype for more flexibility. If the checking succeeds, it returns the calculated type(s) of the expression, along with a list of zero or more proof obligations.
The type(s) of the expression consists of one or more types; it is never the empty list. The list is a singleton when the expression returns a single value, while it is longer when the expression returns a multiple value, where `multiple' is in the same sense as ACL2's mv; recall that Syntheto is a front-end language for ACL2, and so Syntheto's multiple values correspond to ACL2's multiple values.
The proof obligations are organized as a list, instead of a set, just so that the ordering matches the order in which they arise, as the user visually scans the expression. The ordering has no real logical meaning; however, as it should be provable, the ordering is such that each obligation is well-formed in the context of the preceding ones.
The values of this fixtype are also used as result of checking lists of expressions instead of single expressions. In that case, the list of types has a different meaning: each expression is single-valued, and each type in the list corresponds to an expression. When we check the static well-formedness of a list of expressions, they are always required to be single-values, so it is adequate to use a list of types, and not a list of lists of types. In Syntheto, as in ACL2, there are restrictions on the use of multi-valued expressions, e.g. they cannot be passed as arguments to functions; they have to be bound to (multiple) variables first.
See check-expression and mutually recursive companions for details on how the values of this fixtype are used.