|
|
|---|
|
|
|
|---|
Fixtype of Syntheto quantifiers.
This is a tagged union type, introduced by fty::deftagsum.
These are the usual universal and existential quantifiers in logic.
While they have to be part of the language, and are needed in some cases, in many cases users may not explicitly need to use them, using instead constructs that expand into something with quantifiers behind the scenes.