1. 25 Jan, 2018 40 commits
  2. 23 Jan, 2018 40 commits
  3. 14 Jan, 2018 40 commits
  4. 13 Jan, 2018 40 commits
  5. 12 Jan, 2018 40 commits
  6. 10 Jan, 2018 40 commits
  7. 19 Dec, 2017 40 commits
  8. 18 Dec, 2017 40 commits
  9. 17 Dec, 2017 40 commits
  10. 08 Dec, 2017 40 commits
  11. 05 Dec, 2017 40 commits
  12. 04 Dec, 2017 40 commits
  13. 29 Nov, 2017 40 commits
  14. 28 Nov, 2017 40 commits
  15. 22 Nov, 2017 40 commits
  16. 21 Nov, 2017 40 commits
    • Robbert Krebbers's avatar
      Pattern matching notation for monadic binds. · dcd59f13
      Robbert Krebbers authored
      This gets rid of the old hack to have specific notations for pairs
      up to a fixed arity, and moreover allows to do fancy things like:
      
      ```
      Record test := Test { t1 : nat; t2 : nat }.
      
      Definition foo (x : option test) : option nat :=
        ''(Test a1 a2) ← x;
        Some a1.
      ```
      dcd59f13
  17. 20 Nov, 2017 40 commits
  18. 18 Nov, 2017 40 commits