Verified Vector Clocks: An Experience Report, Part 2

Noted. I didn't define that notation, I just simply pasted in what's in the Coq standard library so it would be clear how the triple constructor worked.

Agreed, could use if. I mainly used match with the true/false branches to make it as close to the original Erlang as possible, for readers unfamiliar with the Coq syntax.

It's definitely not implemented in the most-efficient manner.

If you look at the commit history for the repo, a ton of the functions which were normally partially applied had to either be inlined or broken out else it broke the Core Erlang extraction; mainly because it produced code which wouldn't be compiled by the Erlang compiler. Also, I tried writing it to be as close to the original Erlang as possible to make the post a bit more compelling and understandable for Erlang developers familiar with Riak.

However, that being said it should be pretty readable to an OCaml developer:

Here's the link to the first post, which discusses problems with the Core Erlang extraction and the original version of the code: http://christophermeiklejohn.com/coq/erlang/2013/11/04/verif...

Thanks!