Now in this branch we explore the foundations of metacoq extracted into ocaml
similar to the haskell extraction we did previously https://github.com/meta-introspector/th-desugar/tree/rename/Server/MetaCoq
So we want to extract out the idea of the byte, string, and declaration binary tree of declarations and lift those on top of unimath
Now in this branch we explore the foundations of metacoq extracted into ocaml similar to the haskell extraction we did previously https://github.com/meta-introspector/th-desugar/tree/rename/Server/MetaCoq So we want to extract out the idea of the byte, string, and declaration binary tree of declarations and lift those on top of unimath