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 partia

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/verified-vector-clocks-an-experience-report-part-1.html http://christophermeiklejohn.com/coq/erlang/2013/11/04/verif...