Operator overriding in annotations
konnov opened this issue · 0 comments
konnov commented
This feature request was brought in the discussion.
Currently, Apalache allows the user to specify operator overrides as explained here. For example:
OVERRIDE_BIRTH_YEAR == 80
OVERRIDE_LICENSE_AGE == 18
As Markus suggested, this could look much better if annotations were used, e.g.:
\* @overrides("BIRTH_YEAR")
MY_BIRTH_YEAR == 80
\* @overrides("LICENSE_AGE")
MY_LICENSE_AGE == 18