Commits · master · Thibaut Pérami / stdpp

Sep 11, 2023
- Merge branch 'ralf/fmap_inj' into 'master' · b9418660
  Robbert Krebbers authored 1 year ago
  b9418660
- CHANGELOG typo. · 6e97c446
  Robbert Krebbers authored 1 year ago
  6e97c446
- CHANGELOG. · 2db43fb2
  Robbert Krebbers authored 1 year ago
  
  2db43fb2
- Tweaks. · 5b385655
  Robbert Krebbers authored 1 year ago
  
  5b385655
- Add instance `bv_unsigned_inj` and use that. · 415ba1b5
  Robbert Krebbers authored 1 year ago
  
  415ba1b5
Sep 06, 2023
- prove a general option_fmap_inj lemma, and a similar one for lists · b44a2d00
  Ralf Jung authored 1 year ago
  
  b44a2d00
Sep 05, 2023
- Merge branch 'robbert/string_ascii_countable' into 'master' · 1ce70965
  Robbert Krebbers authored 1 year ago
  1ce70965
- CHANGELOG. · e6e864c2
  Robbert Krebbers authored 1 year ago
  
  e6e864c2
- Tweak comments. · f608a1c7
  Ralf Jung authored 1 year ago and Robbert Krebbers committed 1 year ago
  
  f608a1c7
- Comment, rename, make Local. · ffe5989a
  Robbert Krebbers authored 1 year ago
  
  ffe5989a
- Tweak Ltac generator. · d9d623c5
  Robbert Krebbers authored 1 year ago
  
  d9d623c5
- Better `decode` for `string` that is generated. · d08d2b81
  Robbert Krebbers authored 1 year ago
  
  d08d2b81
- Better coding for string/ascii. · dd3b34e2
  Robbert Krebbers authored 1 year ago
  
  dd3b34e2
- Add missing `Local` in `pmap`. · 23d81fe3
  Robbert Krebbers authored 1 year ago
  23d81fe3
Sep 01, 2023
- Merge branch 'bv-notations' into 'master' · 4aa805b7
  Michael Sammler authored 1 year ago
  4aa805b7
- Add bitvector number notations · c4e43577
  Thibaut Pérami authored 1 year ago and Michael Sammler committed 1 year ago
  
  c4e43577
Aug 30, 2023
- Merge branch 'ralf/ge' into 'master' · 92daea78
  Ralf Jung authored 1 year ago
  92daea78
- improve comment · 93177374
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  93177374
- explain why we don't have 'ge' notation · 7286a3cf
  Ralf Jung authored 1 year ago
  
  7286a3cf
Aug 28, 2023
- Merge branch 'ike/hint_mode_leibniz_equiv' into 'master' · 800125de
  Robbert Krebbers authored 1 year ago
  800125de
- Change Hint Mode of LeibnizEquiv · faa43c7a
  Ike Mulder authored 1 year ago
  
  faa43c7a
- more comment tweaks (by Robbert) · 39d0f5b4
  Ralf Jung authored 1 year ago
  
  39d0f5b4
- Merge branch 'ralf/multiset-solver' into 'master' · fe6145b9
  Ralf Jung authored 1 year ago
  fe6145b9
- more precise comment · a95c77fa
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  a95c77fa
- use ssreflect rewrite for multiset tactics · 4395d5a8
  Ralf Jung authored 1 year ago
  
  4395d5a8
Aug 03, 2023
- Merge branch 'fold_comm_acc_lemmas' into 'master' · 4be5fd62
  Robbert Krebbers authored 1 year ago
  4be5fd62
- Ralf's suggestions. · 0d1eb9c1
  Robbert Krebbers authored 1 year ago
  
  0d1eb9c1
- Tweak proofs. · 49189aaa
  Robbert Krebbers authored 1 year ago
  
  49189aaa
- Add fold-commuting lemmas to CHANGELOG.md · 6d5bd7c2
  Isaac van Bakel authored 1 year ago
  
  6d5bd7c2
- Weaken premises and tweak proofs. · 98bbf575
  Robbert Krebbers authored 1 year ago
  
  98bbf575
- Rename comm_acc -> comm_accum · d871b2cf
  Isaac van Bakel authored 2 years ago
  d871b2cf
- Strengthen all fold commutativity lemmas · 5f006e49
  Isaac van Bakel authored 2 years ago
  5f006e49
- Strengthen multiset disj union lemma · 27c24dd4
  Isaac van Bakel authored 2 years ago
  27c24dd4
- Extend fold-commuting lemmas to lists, sets · 584ae69c
  Isaac van Bakel authored 2 years ago
  584ae69c
- Add lemmas for commuting funcs with folds · 66a2fa17
  Isaac van Bakel authored 2 years ago
  66a2fa17
- Merge branch 'robbert/params_lookup' into 'master' · 85778afd
  Robbert Krebbers authored 1 year ago
  85778afd
- Add CHANGELOG. · 5f404bc2
  Robbert Krebbers authored 1 year ago
  
  5f404bc2
- Correct `Params` instances for `lookup` and `singletonM`. · d61d9268
  Robbert Krebbers authored 1 year ago
  
  d61d9268
- Merge branch 'ralf/pair_equiv' into 'master' · 14322a17
  Ralf Jung authored 1 year ago
  14322a17
- Merge branch 'robbert/better_proper' into 'master' · e99461ab
  Ralf Jung authored 1 year ago
  e99461ab