too slow
Opened this issue · 0 comments
aa755 commented
The deductive-style translation of inductive types is too slow. Extracting to OCaml/Haskell and profiling may be an option. There are a lot of duplicate computations. Also, unary numbers are heavily used: even template-Coq uses them.