Skip to content
Snippets Groups Projects
Commit 41044564 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Make (most of) the typing lemmas implications in Iris. 

This requires using iApply instead of eapply to use them.

TODO : have an Iris version of Forall2, so that the lemmas for typing switches can be implications in Iris.
parent c0757d53
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 312 additions and 324 deletions
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment