Skip to content

Draft: binary lexeme backend for coq - with Coq translation

Guillaume Claret requested to merge clarus1/data-encoding:guillaume-claret@binary-lexeme-backend-for-coq into binary-lexeme-backend-for-coq
  • ./build_coq_translation.sh to generate the Coq translation and compile the generated files;
  • may require the development version of coq-of-ocaml;
  • there are some errors during the translation which may be ignored, and the generated Coq code does not compile yet.

Merge request reports