Commits · coq-stdpp-1.0 · Jan / stdpp · GitLab

Snippets Groups Projects

Feb 10, 2017
- Make arguments for sig and sigT constructors and projections maximally implicit. · 613168bf
  Robbert Krebbers authored 8 years ago
  613168bf
Feb 09, 2017
- Prove elem_of_submseteq. · c1687739
  Robbert Krebbers authored 8 years ago
  
  c1687739
- Propers for monadic operations on option. · 0144c537
  Robbert Krebbers authored 8 years ago
  
  0144c537
Feb 07, 2017
- Also support Coq 8.5pl3. · 10c2f692
  Robbert Krebbers authored 8 years ago
  
  10c2f692
Feb 03, 2017
- Make f_equiv stronger. · 2c261344
  Robbert Krebbers authored 8 years ago
  2c261344
Jan 31, 2017
- A bunch of missing Params instances. · 4b0631bb
  Robbert Krebbers authored 8 years ago
  
  4b0631bb
- Operations for converting between maps and collections. · e54b7fe0
  Robbert Krebbers authored 8 years ago
  e54b7fe0
- Curry and uncurry operations on gmap. · 7cd44ad5
  Robbert Krebbers authored 8 years ago
  
  7cd44ad5
- Fold operation on finite maps. · c134e48c
  Robbert Krebbers authored 8 years ago
  
  c134e48c
- Bump year in prelude copyright headers. · a89c6d78
  Robbert Krebbers authored 8 years ago
  
  a89c6d78
- Vector tweaks. · 845e9b73
  Robbert Krebbers authored 8 years ago
  
  845e9b73
- Use primitive projections for sealing · eebf68aa
  Ralf Jung authored 8 years ago
  eebf68aa
- Make instances EqDecision and Countable of gmultiset less eager. · 2e2351cd
  Robbert Krebbers authored 8 years ago
  2e2351cd
- Recursive [inv_vec]. · 3ebeaca2
  Jacques-Henri Jourdan authored 8 years ago
  
  3ebeaca2
- Renaming in prelude/list. · 0158faa7
  Robbert Krebbers authored 8 years ago
  0158faa7
- more restrictive Proof Using hints in (most files of the) prelude · 808b681c
  Ralf Jung authored 8 years ago
  
  808b681c
- Tweak some proof using tweaks for setoid stuff. · 24623c52
  Robbert Krebbers authored 8 years ago
  
  24623c52
- tune "Proof using" directives to minimize differences to previous types of all lemmas · 47e0f1c4
  Ralf Jung authored 8 years ago
  
  47e0f1c4
- don't use Proof Using in a few files that get too many unnecessary annotations from this · ee3e02f0
  Ralf Jung authored 8 years ago
  
  ee3e02f0
- Require `Total R` just for the merge sort theorems that actually need it. · 2028fae1
  Robbert Krebbers authored 8 years ago
  
  2028fae1
- Document list_remove and list_remove_list. · 649f7c76
  Robbert Krebbers authored 8 years ago
  
  649f7c76
- Fix more _L lemmas. · 4fd8d550
  Robbert Krebbers authored 8 years ago
  
  4fd8d550
- make "make quick" quick by adding hints about the used section variables · 108d1f8d
  Ralf Jung authored 8 years ago
  108d1f8d
- add decide_left, decide_right · 50b9555d
  Ralf Jung authored 8 years ago
  
  50b9555d
- Move stuff out of sections that does not depend on the section variables. · cab3033b
  Robbert Krebbers authored 8 years ago
  
  cab3033b
- Simplify proofs relating nth to lookup. · b084730a
  Robbert Krebbers authored 8 years ago
  b084730a
- list: relate nth and lookup · cdcfeee8
  Ralf Jung authored 8 years ago
  
  cdcfeee8
- A few lemmas about vec and fin. · 30b2cbc7
  Jacques-Henri Jourdan authored 8 years ago
  
  30b2cbc7
Dec 09, 2016
- Rename fmap_Some_equiv' → fmap_Some_equiv_1. · d631fdde
  Robbert Krebbers authored 8 years ago
  d631fdde
- rename _setoid suffix to _equiv; add variant of fmap_Some_setoid that can be usefully destructed · 575f23a9
  Ralf Jung authored 8 years ago
  
  575f23a9
Dec 08, 2016
- Fix breaking ee6df099. · a4fe5037
  Robbert Krebbers authored 8 years ago
  a4fe5037
- Optimize simplify_eq. · a07364fc
  Robbert Krebbers authored 8 years ago
  a07364fc
- Avoid exponential blowup in [done] as caused by a7e91677. · 4c6881ab
  Robbert Krebbers authored 8 years ago
  4c6881ab
Dec 06, 2016
- fix compatibility with latest Coq 8.6 · 5c1d2472
  Ralf Jung authored 8 years ago
  
  5c1d2472
- Factor out some common properties about lists. · 090127a0
  Robbert Krebbers authored 8 years ago
  
  090127a0
Dec 05, 2016
- New definition of contractive. · 3caefaaa
  Robbert Krebbers authored 8 years ago
  3caefaaa
Nov 29, 2016
- Some more of_list stuff. · 3f13bd94
  Robbert Krebbers authored 8 years ago
  
  3f13bd94
Nov 24, 2016
- More multiset stuff. · 8f4fe3de
  Robbert Krebbers authored 8 years ago
  
  8f4fe3de
Nov 23, 2016
- Fix typo. · ed15664a
  Robbert Krebbers authored 8 years ago
  
  ed15664a
- Some tweaks to minimal. · b7460a79
  Robbert Krebbers authored 8 years ago
  
  b7460a79