You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
TLA+ has a really rare scoping rule where including the exact same operator more than once is ok and does nothing. We currently would flag this as an error even though it should work in principle.
Example:
module A declares operator foo
module B extends module A
module C extends module A
module D extends modules B and C
D gets one unique copy of operator foo. As it is now, PGo would complain about a redefinition of foo.
The text was updated successfully, but these errors were encountered:
TLA+ has a really rare scoping rule where including the exact same operator more than once is ok and does nothing. We currently would flag this as an error even though it should work in principle.
Example:
foo
D gets one unique copy of operator foo. As it is now, PGo would complain about a redefinition of
foo
.The text was updated successfully, but these errors were encountered: