Open aa755 opened 7 years ago
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.
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.