POPL20 Iris Tutorial merge requestshttps://gitlab.rts.mpi-sws.org/iris/tutorial-popl20/-/merge_requests2020-07-28T16:19:09Zhttps://gitlab.rts.mpi-sws.org/iris/tutorial-popl20/-/merge_requests/1Iris 3.3 port2020-07-28T16:19:09ZArthur Azevedo de AmorimIris 3.3 portI've ported the solution files to work with Iris 3.3 and regenerated the corresponding exercise files. I've tried to update the OPAM recipe to use 3.3, but I haven't tested the script to build the dependencies.I've ported the solution files to work with Iris 3.3 and regenerated the corresponding exercise files. I've tried to update the OPAM recipe to use 3.3, but I haven't tested the script to build the dependencies.https://gitlab.rts.mpi-sws.org/iris/tutorial-popl20/-/merge_requests/2Auto-generate exercise files2020-08-28T10:22:10ZRalf Jungjung@mpi-sws.orgAuto-generate exercise filesThis is the same as https://gitlab.mpi-sws.org/iris/tutorial-popl18/-/merge_requests/4. I slightly adjusted the syntax to be more like what this repository seems to expect, so the exercise generator now understand that `Qed.` typically e...This is the same as https://gitlab.mpi-sws.org/iris/tutorial-popl18/-/merge_requests/4. I slightly adjusted the syntax to be more like what this repository seems to expect, so the exercise generator now understand that `Qed.` typically ends a solution. (I will update the other repository if we agree on this syntax.)
Cc @robbertkrebbershttps://gitlab.rts.mpi-sws.org/iris/tutorial-popl20/-/merge_requests/3Fix a typo in compatibility.v2020-10-10T08:22:59ZFengmin ZhuFix a typo in compatibility.v```
Γ ⊢ (e1, e2) : A1 * A2
```
should be
```
Γ ⊨ (e1, e2) : A1 * A2
``````
Γ ⊢ (e1, e2) : A1 * A2
```
should be
```
Γ ⊨ (e1, e2) : A1 * A2
```