informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
608 stars 30 forks source link

Relax unshadowing for let defs #1444

Closed bugarela closed 1 month ago

bugarela commented 1 month ago

Hello :octocat:

This makes unshadowing smarter so it doesn't have to rename all names, only the ones that are actually shadowing another name.

Unfortunately I could just do it for the let definitions, not for lambdas. See #1443. But this is the most important part, because it fixes names for nondets and nondetPicks looks good (see the test).

I found a couple of problems in our definition collection through testing this, since we rely on more collected metadata to decide what to unshadow now. So there are some small fixes for those as well.