What data types should define new scopes?

[niazim3]

In the comments of commit 6c6e48a, @JacquesCarette mentioned that "We can later decide which things define new scopes (such as DataDefinitions), and make it an error to scope something to an element which does not, in fact, define a scope."

This requires some design and is related to #787.

[balacij]

Following up from the last meeting (#2957), transcribing some discussion:

This ticket is about defining scopes for variables/symbols (but potentially other things too). For many symbols, we do want them in the global namespace, but in many scenarios, we might also want to have non-global (e.g., local) scopes that define symbols for some contexts that we don't want shown globally (e.g., in the SRS' Table of Symbols). Specifically, i, j, and k are symbols we often use locally (with different descriptions). There also exists use-cases for scopes outside of variables/symbols. Namely, for theories, there exists "delta theories" -- situations where a theory opens a new theory with a limited lifetime (restricted to the context of the super theory), very similar to localized variables.

This ticket would be considered "long-term", and would only be resolved when we desperately need it.

[balacij]

I'll close this ticket in favour of #787 because the question will re-occur and the ticket is linked. If anyone feels otherwise, they can re-open it, of course.