logsem / iris-tutorial

MIT License
25 stars 13 forks source link

Typo in definition of step in adequacy.v #2

Closed hei411 closed 1 year ago

hei411 commented 1 year ago

The typo can be found here. Instead of σ1, it should be σ2, since the state of config2 changes.

Similarly, it should be changed in the adequacy.v file in theories/, i.e. here

adamAndMath commented 1 year ago

Fixed