Commits · 07c4f0eeee6bb66baae58ca8349ab2b387befc0e · Iris / stdpp

Oct 20, 2023
- Rename `list_elem_of_fmap_2_alt` → `list_elem_of_fmap_2'`. · 07c4f0ee
  Robbert Krebbers authored 1 year ago
  
  07c4f0ee
- Fix bug in CHANGELOG. · facb9097
  Robbert Krebbers authored 1 year ago
  
  facb9097
- Rename `list_alter_fmap` → `list_fmap_alter`, remove `list_alter_fmap_mono`. · d624ecd7
  Robbert Krebbers authored 1 year ago
  
  d624ecd7
- Also fix `elem_of_list` → `list_elem_of` inconsistency. · 9d2e6d60
  Robbert Krebbers authored 1 year ago
  
  9d2e6d60
Oct 17, 2023
- CHANGELOG. · 44d3349c
  Robbert Krebbers authored 1 year ago
  
  44d3349c
- Make `lookup` and `elem_of` lemmas for `list` consistent with those for map and set. · d9a6e55e
  Robbert Krebbers authored 1 year ago
  
  d9a6e55e
- Merge branch 'robbert/eq_lemmas' into 'ci/refactor_staging' · fead4470
  Robbert Krebbers authored 1 year ago
  
  Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement. See merge request !526
  fead4470
- CHANGELOG. · 0a52e84c
  Robbert Krebbers authored 1 year ago
  
  0a52e84c
Oct 16, 2023
- Follow same scheme for list lemmas. · 211ee09d
  Robbert Krebbers authored 1 year ago
  
  211ee09d
- Follow same scheme for `multiplicity_singleton`. · f85c45f4
  Robbert Krebbers authored 1 year ago
  
  f85c45f4
- Follow same scheme for other map lemmas. · b7eaaf91
  Robbert Krebbers authored 1 year ago
  
  b7eaaf91
Oct 15, 2023
- `_eq` lemmas for maps. · ec2d6bdd
  Robbert Krebbers authored 1 year ago
  
  ec2d6bdd
Oct 14, 2023
- Break long line. · 32edabf7
  Robbert Krebbers authored 1 year ago
  
  32edabf7
- Style tweak. · d4bf79dc
  Robbert Krebbers authored 1 year ago
  
  d4bf79dc
- Merge branch 'robbert/prod_swap' into 'master' · cf73e508
  Ralf Jung authored 1 year ago
  
  Add `prod_swap` and some basic results for it. See merge request !529
  cf73e508
- Merge branch 'robbert/params_prod_map_zip' into 'master' · c6f681e9
  Ralf Jung authored 1 year ago
  
  Missing `Params` instances for `prod_map` and `prod_zip`. See merge request !528
  c6f681e9
- CHANGELOG. · 44f5907d
  Robbert Krebbers authored 1 year ago
  
  44f5907d
- Add `prod_swap` and some basic results for it. · 6588645a
  Robbert Krebbers authored 1 year ago
  
  6588645a
- Missing `Params` instances for `prod_map` and `prod_zip`. · 85c505f5
  Robbert Krebbers authored 1 year ago
  
  85c505f5
- Merge branch 'ralf/inv' into 'master' · f25cad12
  Ralf Jung authored 1 year ago
  
  add inv and oinv tactics that are basically a smarter and fixed inversion_clear Closes #40 See merge request !525
  f25cad12
- changelog · 9a6c8a2b
  Ralf Jung authored 1 year ago
  
  9a6c8a2b
- use the new tactics in a few spots · 9cd88db3
  Ralf Jung authored 1 year ago
  
  9cd88db3
- add inv and oinv tactics that are basically a smarter and fixed inversion_clear · df339448
  Ralf Jung authored 1 year ago
  
  df339448
- Merge branch 'robbert/lt_wf_projected' into 'master' · c4ea1778
  Ralf Jung authored 1 year ago
  
  Add lemmas for easy measure/size induction. See merge request !519
  c4ea1778
- Add test case. · dabf8fc1
  Robbert Krebbers authored 1 year ago
  
  dabf8fc1
- CHANGELOG. · 4901b4b6
  Robbert Krebbers authored 1 year ago
  
  4901b4b6
- Add `lt_wf_projected` lemmas for `nat`, `N`, `Z`. · 4ef46416
  Robbert Krebbers authored 1 year ago
  
  4ef46416
- Merge branch 'ralf/wf' into 'master' · b7c80640
  Robbert Krebbers authored 1 year ago
  
  remove 'wf' alias for the standard 'well_founded' See merge request !524
  b7c80640
- Tweak line breaks. · 64df1cb3
  Robbert Krebbers authored 1 year ago
  
  64df1cb3
- remove 'wf' alias for the standard 'well_founded' · 93b18524
  Ralf Jung authored 1 year ago
  
  93b18524
Oct 13, 2023
- Merge branch 'ralf/solve-proper-subrelation' into 'master' · 03757caf
  Ralf Jung authored 1 year ago
  
  solve_proper: add support for subrelation See merge request !495
  03757caf
- style tweaks · 87514dbe
  Robbert Krebbers authored 1 year ago and Ralf Jung committed 1 year ago
  
  87514dbe
- we do need mode ! and eassumption after all · bb39df76
  Ralf Jung authored 1 year ago
  
  with tests
  bb39df76
- changelog · 20aa2105
  Ralf Jung authored 1 year ago
  
  20aa2105
- try fast_reflexivity first, not last · 4d2b8870
  Ralf Jung authored 1 year ago
  
  4d2b8870
- factor flip cleaning into a tactic · 3705700a
  Ralf Jung authored 1 year ago
  
  and more comments
  3705700a
- move some tactic tests so they can be run with fewer things compiling · 1d5b61f3
  Ralf Jung authored 1 year ago
  
  1d5b61f3
- move flip handling to inside f_equiv and solve_proper_finish · f816088c
  Ralf Jung authored 1 year ago
  
  f816088c
- solve_proper: add support for subrelation · c842d7e2
  Ralf Jung authored 1 year ago
  
  c842d7e2
- Merge branch 'mthrow' into 'master' · 75a2c419
  Robbert Krebbers authored 1 year ago
  
  Add `MThrow` and replace `MGuard` See merge request !522
  75a2c419