pedagand/random-access-list

Binary random-access lists in Coq

This formalization grows a random-access list data-structure out of binary numbers with digits 0 and 1. It is mostly a pedagogical exercise in the study of ornamentation, in the wider context of numerical representations.

To type-check the project, run:

$ make

To produce the documentation, run:

$ make html