• Jakob Botsch Nielsen's avatar
    More efficient list encoding for Countable · 9b209c98
    Jakob Botsch Nielsen authored
    This changes the encoding used for finite lists of values of countable
    types to be linear instead of exponential. The encoding works by
    duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
    separating each element with 10. The top 1-bits are not kept since we
    know a 10 is starting a new element which ends with a 1.
    
    Fix #28
    9b209c98
Name
Last commit
Last update
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
descr Loading commit data...
opam Loading commit data...