Commits · master · Simon Gregersen / stdpp · GitLab

Snippets Groups Projects

May 05, 2021
- add Countable instance for decidable Sigma types · 057543ba
  Simon Gregersen authored Apr 24, 2021
  
  057543ba
May 04, 2021
- Merge branch 'robbert/True_False_lemmas' into 'master' · f7c9c556
  Robbert Krebbers authored May 4, 2021
  f7c9c556
- Apply 1 suggestion(s) to 1 file(s) · e703b4c9
  Robbert Krebbers authored May 4, 2021
  
  e703b4c9
May 03, 2021
- CHANGELOG. · a9fa2606
  Robbert Krebbers authored May 3, 2021
  
  a9fa2606
- Also write `option_guard_True` using `mguard` (instead of `guard` notation). · 5ad12cd3
  Robbert Krebbers authored May 3, 2021
  
  5ad12cd3
- Rename `decide_left` → `decide_True_pi`, `decide_right` → `decide_False_pi`. · 60645f9b
  Robbert Krebbers authored Apr 28, 2021
  
  60645f9b
- Generalize lemma `option_guard_False`. · acb221eb
  Robbert Krebbers authored Apr 28, 2021
  
  acb221eb
- Add lemma `option_guard_True_pi`. · 0160850a
  Robbert Krebbers authored Apr 28, 2021
  
  0160850a
May 02, 2021
- re-enable coq.dev CI · d9aa2025
  Ralf Jung authored May 2, 2021
  
  d9aa2025
Apr 30, 2021
- Merge branch 'ralf/coercions' into 'master' · 3b02de05
  Ralf Jung authored Apr 30, 2021
  3b02de05
Apr 29, 2021
- remove Z.of_nat coercion entirely in std++ (but we'll add it in Iris for now) · 5062a5fc
  Ralf Jung authored Apr 29, 2021
  
  5062a5fc
- make Z.of_nat not a coercion inside the prelude implementation · 91fae00c
  Ralf Jung authored Apr 29, 2021
  
  91fae00c
- disable coq.dev CI as that package is currently broken · 2d7f0238
  Ralf Jung authored Apr 29, 2021
  
  2d7f0238
- Merge branch 'msammler/no_Z_in_rotate' into 'master' · 94a21a33
  Robbert Krebbers authored Apr 29, 2021
  94a21a33
- Don't use Z.to_nat in definition of rotate · 79f6566a
  Michael Sammler authored Apr 29, 2021
  
  79f6566a
- Merge branch 'ralf/Qc_of_Z' into 'master' · a6cfc283
  Ralf Jung authored Apr 29, 2021
  a6cfc283
- changelog · d1d19677
  Ralf Jung authored Apr 29, 2021
  
  d1d19677
- make Qc_of_Z not a Coercion any more · 71091aa2
  Ralf Jung authored Apr 29, 2021
  
  71091aa2
Apr 23, 2021
- Fix comment. Thanks @mpu . · 54252fbc
  Robbert Krebbers authored Apr 23, 2021
  
  54252fbc
Apr 22, 2021
- bump Coq version we test to 8.13.2 · 3652e6e8
  Ralf Jung authored Apr 22, 2021
  
  3652e6e8
Apr 21, 2021
- `Inj` instances for set and multiset singletons. · 0a55fc55
  Robbert Krebbers authored Apr 21, 2021
  
  0a55fc55
- Add `Inj2` instance for singleton on maps. · 47b6bcc0
  Robbert Krebbers authored Apr 21, 2021
  
  47b6bcc0
- Merge branch 'robbert/multiset_notation_tests' into 'master' · a64573ba
  Robbert Krebbers authored Apr 21, 2021
  a64573ba
Apr 20, 2021
- Add pretty printing tests for multiset literals. · 8daabbfc
  Robbert Krebbers authored Apr 20, 2021
  
  8daabbfc
- Fix prettty printing of multiset literals. · f6f3b9c6
  Robbert Krebbers authored Apr 20, 2021
  
  f6f3b9c6
- Merge branch 'robbert/singletonMS' into 'master' · 03290b88
  Robbert Krebbers authored Apr 20, 2021
  03290b88
- CHANGELOG. · 9e9e06d2
  Robbert Krebbers authored Apr 20, 2021
  
  9e9e06d2
- Comment about `SingletonMS` and reorganize a bit. · e4e27935
  Robbert Krebbers authored Apr 20, 2021
  
  e4e27935
- Add lemma `gmultiset_not_elem_of_empty`. · fde7718b
  Robbert Krebbers authored Apr 20, 2021
  
  fde7718b
- Introduce `SingletonMS` class for multiset singletons. · 0120e6fa
  Robbert Krebbers authored Apr 20, 2021
  0120e6fa
- Merge branch 'robbert/subset_difference_elem_of' into 'master' · cc9683cb
  Robbert Krebbers authored Apr 20, 2021
  cc9683cb
- Merge branch 'msammler/list_to_map_app' into 'master' · c6aa1f5f
  Robbert Krebbers authored Apr 20, 2021
  c6aa1f5f
- Add list_to_map_app · 41df24bf
  Michael Sammler authored Apr 15, 2021
  
  41df24bf
- Fix inconsistent arguments of `subset_difference_elem_of`. · 91ea2bfa
  Robbert Krebbers authored Apr 20, 2021
  
  91ea2bfa
Apr 19, 2021
- Merge branch 'msammler/add_hypothesis' into 'master' · 59911631
  Robbert Krebbers authored Apr 19, 2021
  59911631
- Merge branch 'msammler/bounded_testbit' into 'master' · 6412fbd8
  Robbert Krebbers authored Apr 19, 2021
  6412fbd8
- Add lemmas about testbit on bounded integers · c67d6a8f
  Fengmin Zhu authored Apr 15, 2021 and Michael Sammler committed Apr 19, 2021
  
  c67d6a8f
Apr 15, 2021
- Add [learn_hyp_named] and [learn_hyp], fixes #73 · 56a9fc6b
  Michael Sammler authored Apr 15, 2021
  
  56a9fc6b
- Add `map_seq_proper`. · 77cb2b8a
  Robbert Krebbers authored Apr 15, 2021
  
  77cb2b8a
- Merge branch 'improve_prefix_suffix' into 'master' · abee55c9
  Robbert Krebbers authored Apr 15, 2021
  abee55c9