Danil Annenkov
Danil Annenkov
It seems like not all coqdoc comments are handled currently. I run into the following issues: - coqdoc inside definitions renders as comments `(** ... *)` - hiding with `(*...
I've noticed that even with the fastest reduction strategy available - `lazy` - running `tmEval` within the TemplateMonad is still much slower than `vm_compute`. I have an example for which...
If one tries to unquote something like ```Coq Polymorphic Record packType := {pk : Type}. ``` One gets an error like `MetaCoqPolymophicTest.502`. It's related to the names in the polymorphic...
It would be nice to make MetaCoq compatible with the HoTT library (https://github.com/HoTT/HoTT). I know that @andreaslyn would be interested in this kind of compatibility. I guess, making translations to...
I've stumbled upon the following issue. `Derive` fails when I try to use it on something like this: ```coq Record D := { Address : Type}. Inductive msg {d :...
`Derive` for records produces ill-formed code. ```coq Record SimpleRec := { field1 : nat }. Derive Show for SimpleRec. ``` Gives an error ``` Recursive definition of aux is ill-formed....
Variant types cannot be recursive in Liquidity. That means that it is not possible to define custom types like `list` or `tree`. For `list` one can use built-in lists, of...
Currently, Liquidity imposes some constraints on recursive function definitions * Recursive functions can only be tail-recursive. * Recursive functions take a single argument. Are there any plans to improve the...
I hit the following issue when using closures in Liquidity. The example below does not compile giving `Types ((int -> int)[@closure :int]) and int -> int are not compatible` ```OCaml...
I have the following questions: - Will CertiCoq support the use of Coq's primitive integers in a way that they compile to efficient C representation? - More generally, would it...