|
|
|---|
|
|
|
|---|
Fixtype of Syntheto type subsets.
This is a product type introduced by fty::defprod.
This is a subset of another type. It consists, syntactically, of the supertype and an expression that must be boolean-valued and must have a single free variable of the supertype.
This is related to the invariants of type products, but it is convenient to have (optional) invariants in the type products, rather than forcing the user to give a name to the product without invariant and then define the subtype of the product type.
The field
A type subset also includes an optional witness expression. If present, this must be a ground expression that evaluates to a value satisfying the restriction. If absent, such an expression must be inferred in some way. This witness is needed to show that the subtype is inhabited, which is used to defined the fixer of the ACL2 fixtype generated for the Syntheto fixtype.