mcqc

mcqc copied to clipboard

Should be: Coq struct type declarations -> C struct type declarations + accessor functions

elefthei

Currying is easily supported and experiments show lambdas are elaborated at compile time by clang++, use `curry()` in `include/curry.h`.

elefthei

Instead of being ``` template using list = std::variant ``` Make it be ``` template using list = std::shared_ptr ``` Which makes `addPtr` redundant, a good thing!

elefthei

Cyclical recursive references of constructors is a problem. Hopefully, forward declaration in C++ works, so the following for a list is better ``` template struct Coq_nil; template struct Coq_cons; template...

elefthei

Right now, substituting free types is not kept in context as a constraint and thus we cannot do constraint solving. Add `CTFree` constraints in the context and remove them according...

elefthei

Fixpoint expressions are annoying, because they capture the enclosing scope and must be outlined together with their scope references to work in C++

elefthei

Context is now a map, which does not allow for two polymorphic definitions to coexist, although clang clearly allows that (overloading). Substitute Map for Multimap in Context definition. http://hackage.haskell.org/package/multimap-1.2.1/docs/Data-MultiMap.html

elefthei

Induction principles extract to ill-typed C++ code

7

Here is an example Coq program: ```coq Module Tree. Inductive tree (A : Type) := | leaf : tree A | node : A -> tree A -> tree A...

joom