Commits · master · Iris / stdpp

Apr 08, 2025
- make coq-lint nix-compatible · 39860d00
  Ralf Jung authored 4 days ago
  
  39860d00
Mar 30, 2025
- Merge branch 'ralf/list-split' into 'master' · 9274984b
  Ralf Jung authored 1 week ago
  
  split up list.v into smaller files See merge request !594
  9274984b
Mar 29, 2025
- CHANGELOG. · 74ed6cfa
  Robbert Krebbers authored 2 weeks ago
  
  74ed6cfa
- Move `list_find` to misc. · e400a5b1
  Robbert Krebbers authored 2 weeks ago
  
  (Note: rename some bound variables to avoid conflicts with `Implicit Types`.)
  e400a5b1
- Move `discriminate_list` and `simplify_list_eq` to basics. · 9dc6a84e
  Robbert Krebbers authored 2 weeks ago
  
  9dc6a84e
- Self contained proof of `submseteq_dec` and move to correct file. · 34e5f70a
  Robbert Krebbers authored 2 weeks ago
  
  34e5f70a
- Fix comment that is messed up. · db8b426e
  Robbert Krebbers authored 2 weeks ago
  
  db8b426e
Mar 28, 2025
- Move filter lemmas to basics. · dc158f6f
  Robbert Krebbers authored 2 weeks ago
  
  dc158f6f
- changelog · 42b0adeb
  Ralf Jung authored 2 weeks ago
  
  42b0adeb
- move NoDup lemmas into list_relations · 85ad825c
  Ralf Jung authored 2 weeks ago
  
  85ad825c
- split up list.v into smaller files · 3bc47928
  Ralf Jung authored 2 weeks ago
  
  3bc47928
- Merge branch 'ralf/no-notypeclasses-apply' into 'master' · 72579d23
  Ralf Jung authored 2 weeks ago
  
  remove notypeclasses apply; it is somehow very slow See merge request !592
  72579d23
- remove notypeclasses apply; it is somehow very slow · af70e2de
  Ralf Jung authored 2 weeks ago
  
  af70e2de
Mar 24, 2025
- Merge branch 'marijnvanwezel/SetUnfoldElemOf_dom_gmultiset' into 'master' · 95b6b0c0
  Ralf Jung authored 2 weeks ago
  
  Add `SetUnfoldElemOf` instance of `dom` on `gmultiset` See merge request !591
  95b6b0c0
Mar 12, 2025
- Add test and update CHANGELOG · 713ad87c
  Marijn van Wezel authored 1 month ago
  
  713ad87c
- Add `SetUnfoldElemOf` instance of `dom` on `gmultiset` · 5db505ac
  Marijn van Wezel authored 1 month ago
  
  5db505ac
Feb 26, 2025
- Merge branch 'marijnvanwezel/StronglySorted_app' into 'master' · d2e8771d
  Robbert Krebbers authored 1 month ago
  
  Add lemma `StronglySorted_app_iff` See merge request !584
  d2e8771d
Feb 25, 2025
- Tweak imports · 7d1f381e
  Marijn van Wezel authored 1 month ago
  
  7d1f381e
- Tweak CHANGELOG. · 80ff9d7b
  Robbert Krebbers authored 1 month ago and Marijn van Wezel committed 1 month ago
  
  80ff9d7b
- Renames and make use of `set_solver` to shorten proof. · 55e93ffd
  Robbert Krebbers authored 1 month ago and Marijn van Wezel committed 1 month ago
  
  55e93ffd
- Add lemma `StronglySorted_app` · 7f43d3f2
  Marijn van Wezel authored 2 months ago and Marijn van Wezel committed 1 month ago
  
  7f43d3f2
- Merge branch 'kimaya/add-seq-lemmas' into 'master' · 6ac98356
  Ralf Jung authored 1 month ago
  
  add lemmas about seq See merge request !588
  6ac98356
Feb 20, 2025
- Apply 1 suggestion(s) to 1 file(s) · a9167769
  Kimaya Bedarkar authored 1 month ago
  
  Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
  a9167769
- Apply 1 suggestion(s) to 1 file(s) · ffcb6d4d
  Kimaya Bedarkar authored 1 month ago
  
  Co-authored-by: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
  ffcb6d4d
Feb 19, 2025
- add lemmas about seq · 0fb1c214
  Kimaya Bedarkar authored 1 month ago
  
  0fb1c214
Feb 18, 2025
- More CoqDoc. · 0dbb3948
  Robbert Krebbers authored 1 month ago
  
  0dbb3948
- Merge branch 'ralf/gen-tree' into 'master' · d99d3967
  Ralf Jung authored 1 month ago
  
  gen_tree: add comment explaining intended usage See merge request !587
  d99d3967
- improve comment · 3b269ef3
  Ralf Jung authored 1 month ago
  
  3b269ef3
Feb 17, 2025
- Merge branch 'kimaya/add-zip-lemmas' into 'master' · 6d3e54a8
  Ralf Jung authored 1 month ago
  
  add some zip lemmas See merge request !582
  6d3e54a8
- add some zip lemmas · 53b54c52
  Kimaya Bedarkar authored 1 month ago and Ralf Jung committed 1 month ago
  
  53b54c52
- gen_tree: add comment explaining intended usage · b38cea43
  Ralf Jung authored 1 month ago
  
  b38cea43
Feb 12, 2025
- ref tests: stop printing diff when it is ignored anyway · 0b8ac81f
  Ralf Jung authored 1 month ago
  
  0b8ac81f
Feb 07, 2025
- Merge branch 'ralf/notc-apply-no-hnf' into 'master' · cc5fd623
  Ralf Jung authored 2 months ago
  
  notypeclasses apply: do not unfold the type See merge request !586
  cc5fd623
- minor nits · 59643c49
  Ralf Jung authored 2 months ago
  
  59643c49
- notypeclasses apply: do not unfold the type · 8dd38309
  Ralf Jung authored 2 months ago
  
  also improve the error message
  8dd38309
- Merge branch 'ralf/notypeclasses-apply-docs' into 'master' · de2bf2a5
  Robbert Krebbers authored 2 months ago
  
  notypeclasses apply: fix comment See merge request !585
  de2bf2a5
Feb 06, 2025
- notypeclasses apply: fix comment · 233acb0d
  Ralf Jung authored 2 months ago
  
  233acb0d
Feb 05, 2025
- Merge branch 'ci/msammler/_1_2_lemmas' into 'master' · 96ef0cd6
  Robbert Krebbers authored 2 months ago
  
  Add some _1, _2 lemmas for map_filter See merge request !394
  96ef0cd6
- Add _1, _2 lemmas for map_empty_filter · 5a5578b4
  Michael Sammler authored 2 months ago
  
  5a5578b4
Feb 04, 2025
- Merge branch 'ralf/notypeclasses-apply' into 'master' · ada66bd2
  Ralf Jung authored 2 months ago
  
  add 'notypeclasses apply' tactic Closes #220 See merge request iris/stdpp!581
  ada66bd2