search

hwayne / learntla

A TLA+ guide
http://www.learntla.com
Creative Commons Attribution 4.0 International
278 stars 57 forks source link

Make the capture variable different from the free variable to make less confusing #71

Closed hwayne closed 2 years ago

hwayne commented 5 years ago

in the InSensical declaration on the Models->Constraints page, you use ‘tower’ as a variable name scoped to the declaration, but in the larger context of the Hanoi problem, the variable ‘tower’ already has been defined global to the spec which seems like it should make the parser unhappy.

Not a bug, just confusing

https://learntla.com/models/constants/