1. 18 Dec, 2016 3 commits
  2. 16 Dec, 2016 3 commits
  3. 15 Dec, 2016 1 commit
  4. 14 Dec, 2016 6 commits
  5. 13 Dec, 2016 6 commits
  6. 12 Dec, 2016 17 commits
  7. 11 Dec, 2016 1 commit
  8. 09 Dec, 2016 3 commits
    • Ralf Jung's avatar
      move everything to subfolder theories/ · 6b8069fa
      Ralf Jung authored
      6b8069fa
    • Ralf Jung's avatar
      rename rules -> op_rules · 7b14d6a7
      Ralf Jung authored
      Really, *all* of our files contain proof rules
      7b14d6a7
    • Ralf Jung's avatar
      Merge branch 'list-agree' into 'master' · 741c6a8a
      Ralf Jung authored
      Use agree instead of dec_agree
      
      This demonstrates that a list-based agreement could work, and form an OFE. I didn't bother to prove all the functor laws.
      
      Man, this reasoning with about the lists is annoying^^.
      
      What I don't like about this is that un-injection (`agree_car`) is only non-expansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works.
      
      Cc @jjourdan @robbertkrebbers
      
      See merge request !22
      741c6a8a