Commits · a5dc9c2e4fc6bd0e1894392b4ad1cc2445ee98d7 · Iris / stdpp

Aug 11, 2022
- test against upcoming Coq 8.16 · a5dc9c2e
  Ralf Jung authored 2 years ago
  
  a5dc9c2e
- Merge branch 'vsiles' into 'master' · 67890e47
  Robbert Krebbers authored 2 years ago
  
  [list] restricted version of list_fmap_equiv_ext See merge request !384
  67890e47
- fix typo · 1cf6659d
  Michael Sammler authored 2 years ago
  
  1cf6659d
- [list] squashing MR on top of master · ed3c2a92
  Vincent Siles authored 2 years ago
  
  ed3c2a92
- Merge branch 'master' of gitlab.mpi-sws.org:iris/stdpp · 809dee91
  Robbert Krebbers authored 2 years ago
  
  809dee91
- CHANGELOG fix. · 24074da3
  Robbert Krebbers authored 2 years ago
  
  24074da3
- Merge branch 'robbert/list_proper' into 'master' · 66a28855
  Robbert Krebbers authored 2 years ago
  
  Generalize Propers for lists / Add some missing Params See merge request !407
  66a28855
- Fix `Params` for `alter` and add a test. · 0387d97b
  Robbert Krebbers authored 2 years ago
  
  0387d97b
- Add some tests for backwards compatibility. · cce709e0
  Robbert Krebbers authored 2 years ago
  
  cce709e0
- Use "higher-order" propers for list operations. · c67f7331
  Robbert Krebbers authored 2 years ago
  
  c67f7331
- Add missing `Params` instances. · d40e0d65
  Robbert Krebbers authored 2 years ago
  
  d40e0d65
Aug 10, 2022
- Merge branch 'ci/msammler/stdpp_experimental' into 'master' · 06909b86
  Ralf Jung authored 2 years ago
  
  Create stdpp-unstable package and add bitblast library See merge request !402
  06909b86
- tweak · 0d6ed2bf
  Ralf Jung authored 2 years ago
  
  0d6ed2bf
- Create stdpp-unstable package and add bitblast library · 2647c9d8
  Michael Sammler authored 2 years ago
  
  2647c9d8
Aug 09, 2022
- Some tweaks to the structure/proofs of `sets` file. · 02fd8ca3
  Robbert Krebbers authored 2 years ago
  
  02fd8ca3
- Make more use of `@{C}` notation. · b95a6234
  Robbert Krebbers authored 2 years ago
  
  b95a6234
- Move order in `fin_maps`. · 369d9096
  Robbert Krebbers authored 2 years ago
  
  Some `filter` lemmas make use of `map_Forall`, so put `map_Forall` before `filter.
  369d9096
- Merge branch 'set_bind' into 'master' · 42af9985
  Robbert Krebbers authored 2 years ago
  
  Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting See merge request !406
  42af9985
- Add names to CHANGELOG · 38a93520
  Paolo G. Giarrusso authored 2 years ago
  
  38a93520
- Formatting review · db5e0008
  Robbert Krebbers authored 2 years ago and Paolo G. Giarrusso committed 2 years ago
  
  db5e0008
- set_bind_subset -> set_bind_mono · 693458bb
  Paolo G. Giarrusso authored 2 years ago
  
  693458bb
- set_bind theory: revise setoid rewriting · feb655ce
  Paolo G. Giarrusso authored 2 years ago
  
  - strengthen set_bind_subset to have the same arity - add missing Params instance to prevent slow failures in setoid rewriting - `Proper` instances can be proven before `set_bind_ext` via `set_solver`. - `set_bind_ext` is then provable by set_solver directly.
  feb655ce
- Apply some sugguestions from Robbert and Paolo · bcc9161a
  Dan Frumin authored 2 years ago and Paolo G. Giarrusso committed 2 years ago
  
  bcc9161a
- Update the CHANGELOG · 13c3510c
  Dan Frumin authored 2 years ago and Paolo G. Giarrusso committed 2 years ago
  
  13c3510c
- Introduce `set_bind` and associated lemmas. · f4072243
  Dan Frumin authored 2 years ago and Paolo G. Giarrusso committed 2 years ago
  
  f4072243
- Merge branch 'ci/msammler/map_seqZ' into 'master' · f844da54
  Robbert Krebbers authored 2 years ago
  
  Add map_seqZ See merge request !391
  f844da54
Aug 08, 2022
- Merge branch 'msammler/more_1_2_lemmas' into 'master' · f9ee8400
  Robbert Krebbers authored 2 years ago
  
  Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None See merge request !405
  f9ee8400
- Add _1, _2 lemmas for not_elem_of_dom and lookup_union_None · 05c58b27
  Michael Sammler authored 2 years ago
  
  05c58b27
- More general `insert` lemmas for `map_seq`/`map_seqZ`. · 65845b69
  Robbert Krebbers authored 2 years ago and Michael Sammler committed 2 years ago
  
  65845b69
- Add map_seqZ · 29efb9f7
  Michael Sammler authored 2 years ago
  
  29efb9f7
Aug 03, 2022
- Merge branch 'ci/msammler/lookup_union_l' into 'master' · b99e79cf
  Robbert Krebbers authored 2 years ago
  
  Add lookup_union_l' See merge request !395
  b99e79cf
- Rename lookup_union_l' to lookup_union_l and add lookup_union_l dual to lookup_union_r · 8288632b
  Michael Sammler authored 2 years ago
  
  8288632b
Aug 01, 2022
- Merge branch 'ci/msammler/map_agree' into 'master' · beee46c8
  Robbert Krebbers authored 2 years ago
  
  Add map_agree See merge request !392
  beee46c8
- Add CHANGELOG · 05281d98
  Michael Sammler authored 2 years ago
  
  05281d98
- Tweak some proofs. · c0f8d45c
  Robbert Krebbers authored 2 years ago and Michael Sammler committed 2 years ago
  
  c0f8d45c
- Add map_agree · ad2023ed
  Michael Sammler authored 2 years ago
  
  ad2023ed
- Merge branch 'robbert/map_disjoint_fmap' into 'master' · 6f1ca045
  Robbert Krebbers authored 2 years ago
  
  Flip direction of `map_disjoint_fmap`. See merge request !398
  6f1ca045
- CHANGELOG. · 9198e66b
  Robbert Krebbers authored 2 years ago
  
  9198e66b
- Flip direction of `map_disjoint_fmap`. · 7ef1770c
  Robbert Krebbers authored 2 years ago
  
  7ef1770c
- Merge branch 'ci/msammler/list_subseteq_dec' into 'master' · 9d78117d
  Robbert Krebbers authored 2 years ago
  
  Add list_subseteq_dec See merge request !400
  9d78117d