Xia Li-yao

Thanks Andrew, that's a nice explanation!

Also, why is `QcDefaultNotation` distinct from `QcDoNotation`?

I agree avoiding double underscores seems quite inconvenient so it would be preferable to push for a more accommodating convention on Coq's side, and in the meantime to silence the...

There are also some C files to be included for the `external` definitions. BTW Why are there both `float64_31` and `float64_63`? Aren't OCaml `float` guaranteed to be 64 bit? >...

I'm not sure I packaged the C code properly yet. ~~How do I solve ```undefined reference to `coq_uint63_to_float'``` when building an executable using coq-primitive?~~ EDIT: I had included the wrong...

There isn't much duplication. It's mainly moving `coq_float64.c` and two C functions to implement `Uint63.to_float` that are not used anywhere else. There are just two macros being copied, which are...

@Sakarah @maximedenes @silene @proux01 @ppedrot @erikmd This PR relicenses the implementation of primitive ints, floats, and arrays, from LGPL-2.1-only to MIT. Those files are recent enough that their contributors can...

Thanks for the help. It seems the current errors have to do with native compilation not finding the dependencies. Maybe they should be mentioned somewhere around here: https://github.com/coq/coq/blob/4c713ddcf0ebded388b9349938f4371c9c1a254e/kernel/nativelib.ml#L69-L70 except that...

Yes but it uses the terrible unary encoding. I'm also working on making QuickChick executable natively in Coq.

Using `int` rather than `nat` when the unboundedness is not essential would help us avoid accidental quadratic (or exponential) complexity like in #252