|
|
|---|
|
|
|
|---|
Fixtype of semantic assertions.
This is a product type introduced by fty::defprod.
These are the assertions mentioned in semantics-deeply-embedded. They are essentially logical formulas, asserting that the mathematical semantic function returns the boolean `true' on the given inputs.
The components of the assertions defined here correspond to the inputs of the mathematical semantic function sketched in semantics-deeply-embedded, with the exception of the list of definitions. This is left implicit in the assertions, because it would be the same in all of them, and so it is provided externally; see constraint-satp.