Commits · 6c6267a2b8272d2151c6470d8f4b676b0696b1b8 · Iris / stdpp

Sep 06, 2021
- Add a complexity test · 6c6267a2
  Tej Chajed authored 4 years ago
  
  6c6267a2
- Add a more substantial reduction test · 73b4ee3b
  Tej Chajed authored 4 years ago
  
  73b4ee3b
- Use SProp for Pmap and gmap sigma types · 1a98fc89
  Tej Chajed authored 4 years ago
  
  1a98fc89
- Merge branch 'ralf/list_in_dec' into 'master' · 64419715
  Ralf Jung authored 3 years ago
  
  add lemma list_in_dec See merge request !319
  64419715
- Merge branch 'ralf/Forall2' into 'master' · a3841e4d
  Ralf Jung authored 3 years ago
  
  treat Forall2 constructors like we treat Forall constructors See merge request !318
  a3841e4d
- Apply 2 suggestion(s) to 1 file(s) · 68f87208
  Robbert Krebbers authored 3 years ago and Ralf Jung committed 3 years ago
  
  68f87208
- Shorter proof for ∃, also add proof for ∀. · 6f19c369
  Robbert Krebbers authored 3 years ago
  
  6f19c369
- add lemma list_in_dec · 6f401061
  Ralf Jung authored 3 years ago
  
  6f401061
Sep 05, 2021
- Merge branch 'ralf/dom-size' into 'master' · 7d2c8d9a
  Ralf Jung authored 3 years ago
  
  relate size of map to size of its domain See merge request !320
  7d2c8d9a
- changelog · 551b4882
  Ralf Jung authored 3 years ago
  
  551b4882
- make name more consistent · 3303ec5e
  Ralf Jung authored 3 years ago
  
  3303ec5e
- relate size of map to size of its domain · 407d8414
  Ralf Jung authored 3 years ago
  
  407d8414
- Merge branch 'ralf/map_size_disj_union' into 'master' · 608a079a
  Ralf Jung authored 3 years ago
  
  add map_size_disj_union See merge request !321
  608a079a
- changelog · d8db31da
  Ralf Jung authored 3 years ago
  
  d8db31da
- use a different work-around · 1e1dbb14
  Ralf Jung authored 3 years ago
  
  1e1dbb14
- tweak comments; changelog · b4f29dc0
  Ralf Jung authored 3 years ago
  
  b4f29dc0
Aug 11, 2021
- add map_size_disj_union · d4665398
  Ralf Jung authored 3 years ago
  
  d4665398
Jul 29, 2021
- treat Forall2 constructors like we treat Forall constructors · 22015a0e
  Ralf Jung authored 3 years ago
  
  22015a0e
Jul 28, 2021
- Merge branch 'ralf/empy_inv' into 'master' · 10ba5946
  Ralf Jung authored 3 years ago
  
  bring back some empty_inv lemmas for rewriting See merge request !317
  10ba5946
- update sed script · 79bf64ed
  Ralf Jung authored 3 years ago
  
  79bf64ed
- bring back some empty_inv lemmas for rewriting · 5f95d3dd
  Ralf Jung authored 3 years ago
  
  5f95d3dd
- Merge branch 'ralf/relations' into 'master' · a6d2be96
  Ralf Jung authored 3 years ago
  
  relations lemmas See merge request !316
  a6d2be96
- Merge branch 'ralf/lookup-union-difference' into 'master' · 6688588a
  Ralf Jung authored 3 years ago
  
  add some lookup_{union,difference} lemmas See merge request !315
  6688588a
- relations lemmas · dbd58457
  Ralf Jung authored 3 years ago
  
  dbd58457
- changelog · 90b61523
  Ralf Jung authored 3 years ago
  
  90b61523
- make names more consistent · 53e4f0f7
  Ralf Jung authored 3 years ago
  
  53e4f0f7
- shorter proof · 3983fa93
  Robbert Krebbers authored 3 years ago and Ralf Jung committed 3 years ago
  
  3983fa93
- add some lookup_{union,difference} lemmas · 60f310e6
  Ralf Jung authored 3 years ago
  
  60f310e6
- Merge branch 'ralf/get_head' into 'master' · 28ed75d0
  Ralf Jung authored 3 years ago
  
  add get_head tactic and use it in solve_proper_unfold See merge request !311
  28ed75d0
- changelog · ff1aafac
  Ralf Jung authored 3 years ago
  
  ff1aafac
- this is purely syntactic · 093e0481
  Ralf Jung authored 3 years ago
  
  093e0481
- add get_head tactic and use it in solve_proper_unfold · 6ca0d948
  Ralf Jung authored 3 years ago
  
  6ca0d948
- fix build on Coq 8.10 · 653c819a
  Ralf Jung authored 3 years ago
  
  653c819a
- Merge branch 'ralf/insert_map_seq_0' into 'master' · a83b4604
  Ralf Jung authored 3 years ago
  
  add insert_map_seq_0 See merge request !314
  a83b4604
- Merge branch 'ralf/lookup_take_Some' into 'master' · 9faffcdd
  Ralf Jung authored 3 years ago
  
  add lookup_take_Some See merge request !313
  9faffcdd
- Merge branch 'ralf/binder_list' into 'master' · adcb72fd
  Ralf Jung authored 3 years ago
  
  add binder_list See merge request !312
  adcb72fd
- Merge branch 'gset-simpl-never' into 'master' · ac04787b
  Robbert Krebbers authored 3 years ago
  
  Mark gset methods as simpl never to stop `cbn` from unfolding them See merge request !298
  ac04787b
- Changelog · 1ecabad2
  Paolo G. Giarrusso authored 3 years ago
  
  Verified
  
  1ecabad2
- add insert_map_seq_0 · 31e8abdd
  Ralf Jung authored 3 years ago
  
  31e8abdd
- add lookup_take_Some · 90d70690
  Ralf Jung authored 3 years ago
  
  90d70690