Commits · f3091cc36df45fe575d03854d04b5d9c373a3f8e · Iris / stdpp

Oct 24, 2024
- silence some warnings on coq.dev that we cannot fix yet · f3091cc3
  Ralf Jung authored 4 months ago
  
  f3091cc3
Oct 21, 2024
- Merge branch 'marijn/gmultiset_map' into 'master' · 4d307c87
  Ralf Jung authored 4 months ago
  
  Add `gmultiset_map` and associated lemmas See merge request !577
  4d307c87
Oct 18, 2024
- CHANGELOG. · 862e4bc5
  Robbert Krebbers authored 4 months ago
  
  862e4bc5
- Version of `gmultiset_map` that avoids converting to lists. · bfc40224
  Robbert Krebbers authored 4 months ago
  
  bfc40224
Oct 17, 2024
- Move definition to top · 63835cb3
  Marijn van Wezel authored 4 months ago
  
  Unverified
  
  63835cb3
- Rewrite injectivity lemma to instance of Inj · f2098383
  Marijn van Wezel authored 4 months ago
  
  Unverified
  
  f2098383
- Improve styling · e7405db5
  Marijn van Wezel authored 4 months ago
  
  Unverified
  
  e7405db5
- Slightly simplify proof · 2cbe4b4f
  Marijn van Wezel authored 4 months ago
  
  Unverified
  
  2cbe4b4f
- Use unicode arrow · 3f7421c7
  Marijn van Wezel authored 4 months ago
  
  Unverified
  
  3f7421c7
Oct 10, 2024
- Add lemma about injectivity of gmultiset_map when 'f' is injective · 65f28290
  Marijn van Wezel authored 5 months ago
  
  65f28290
- Actually give an explicit name to the IH · 88a3baa1
  Marijn van Wezel authored 5 months ago
  
  88a3baa1
- Explicitly name IH · 70772e14
  Marijn van Wezel authored 5 months ago
  
  70772e14
- Remove superfluous type hints · a1d0c311
  Marijn van Wezel authored 5 months ago
  
  a1d0c311
- Move to section and add lemmas · bb981de3
  Marijn van Wezel authored 5 months ago
  
  bb981de3
Oct 09, 2024
- Add definition for `gmultiset_map` · 65cf7d06
  Marijn van Wezel authored 5 months ago
  
  65cf7d06
Oct 02, 2024
- add comment in _CoqProject · 1fa37d0a
  Ralf Jung authored 5 months ago
  
  1fa37d0a
- Merge branch 'robbert/map_Forall2_nested' into 'master' · 2dd41ab5
  Robbert Krebbers authored 5 months ago
  
  Enable `map_Forall2` to be used in nested inductive relations See merge request !575
  2dd41ab5
Sep 29, 2024
- Also add a test for `map_Forall`. · 5e36b905
  Robbert Krebbers authored 5 months ago
  
  5e36b905
Sep 28, 2024
- Enable `map_Forall2` to be used in nested inductive relations. · 6bb1fc01
  Robbert Krebbers authored 5 months ago
  
  6bb1fc01
Sep 11, 2024
- sync dune flags · bc4fce09
  Ralf Jung authored 6 months ago
  
  bc4fce09
- Merge branch 'robbert/deprecate_rev_length' into 'master' · 6a0896a2
  Ralf Jung authored 6 months ago
  
  Unsilence deprecation warning regarding list lemmas. See merge request !574
  6a0896a2
- move COQ_REF further up so it is easier to see · d297a432
  Ralf Jung authored 6 months ago
  
  d297a432
- Unsilence deprecation warning regarding list lemmas. · 2db35c48
  Robbert Krebbers authored 6 months ago
  
  2db35c48
- test coq 8.19.1 · 8a031c06
  Ralf Jung authored 6 months ago
  
  8a031c06
- switch reftesting to Coq 8.20 · f894e0cf
  Ralf Jung authored 6 months ago
  
  f894e0cf
- silence another warning · f6973baf
  Ralf Jung authored 6 months ago
  
  f6973baf
- silence Coq 8.20 deprecation warnings · 21aaa5d3
  Ralf Jung authored 6 months ago
  
  21aaa5d3
- test Coq 8.20 · 5da2f2e2
  Ralf Jung authored 6 months ago
  
  5da2f2e2
Sep 10, 2024
- Merge branch 'robbert/set_fold_union' into 'master' · a1a12e00
  Robbert Krebbers authored 6 months ago
  
  Add `set_fold_union_strong` and similarly for map See merge request !417
  a1a12e00
- Comments. · 8bfd5a08
  Robbert Krebbers authored 6 months ago
  
  8bfd5a08
- CHANGELOG. · 919f61f7
  Robbert Krebbers authored 6 months ago
  
  919f61f7
- Also add union lemmas for `map_fold`. · 94ea2e33
  Robbert Krebbers authored 6 months ago
  
  94ea2e33
- Add lemmas `set_fold_union_strong` and `set_fold_union`. · c0b1ec66
  Robbert Krebbers authored 2 years ago
  
  c0b1ec66
- Add lemma `foldr_idemp`. · 47a3477b
  Robbert Krebbers authored 2 years ago
  
  47a3477b
- Merge branch 'robbert/string_notation' into 'master' · bc76f1d5
  Robbert Krebbers authored 6 months ago
  
  Better use of modules / less global polution for strings See merge request !570
  bc76f1d5
- Tweak CHANGELOG. · 1dd6bcab
  Robbert Krebbers authored 6 months ago
  
  1dd6bcab
- CHANGELOG. · 420bd785
  Robbert Krebbers authored 6 months ago
  
  420bd785
- Add order on strings. · 560412f0
  Robbert Krebbers authored 6 months ago
  
  560412f0
- Better use of modules for string, consistent with numbers. · c8de231b
  Robbert Krebbers authored 6 months ago
  
  c8de231b
- Merge branch 'robbert/foldr_cons_permute' into 'master' · 2a3b41ca
  Robbert Krebbers authored 6 months ago
  
  Make `foldr_cons_permute` lemmas consistent. See merge request !573
  2a3b41ca