Lookup total lemmas (!125) · Merge requests · Iris / stdpp · GitLab

Snippets Groups Projects

Merged Robbert Krebbers requested to merge robbert/lookup_total_lemmas into master 5 years ago

Mar 17, 2020
- More CHANGELOG. · 97079040
  Robbert Krebbers authored 5 years ago
  
  97079040
- CHANGELOG. · f05baf13
  Robbert Krebbers authored 5 years ago
  
  f05baf13
- Lemmas for `!!!` on lists. · 7ab0cff7
  Robbert Krebbers authored 5 years ago
  
  7ab0cff7
- Lemmas for `!!!` on `∅`, `delete`, `<[_:=_]>`, and `alter` operations on maps. · b3318a08
  Robbert Krebbers authored 5 years ago
  
  For other operations, like `<$>`, such lemmas appear to make little sense, since they require premises involving `!!`.
  b3318a08