Bas Spitters

@CohenCyril there is now also this Nominal Sets library: https://arxiv.org/pdf/2509.25883

This is a great contribution. @4ever2 has reviewed it, so feel free to move ahead, but please add documentation first :-) Could you elaborate on this: > Custom reasoning about...

Have you considered the lean search tools? https://leansearch.net/ (https://github.com/leanprover-community/LeanSearchClient) https://www.leanexplore.com/ https://loogle.lean-lang.org/ https://www.moogle.ai/ It would be nice to have something along these lines for Rocq. I guess that my be connected...

@ndcroos thanks. Please go ahead and do the environment as Karl suggests. it would be great if fast done could be used. from my phone On Sat, Jul 27, 2024,...

@mattam82 This looks exciting! Do you also plan a verified_native_compute based on malfunction? Perhaps, one could do the same for CertiCoq, which would be a possibility to inline C-code, perhaps...

Thanks! As Lasse says a small table of contents, as is usual in MathComp might be helpful. Here is a very detailed style guide for MC. No need to follow...

Yes, that would be great. Also, MC proofs are expected to be read while replaying them, so no need for elaborate documentation in proofs. However, helpful comments are always welcome....

Should be revisited after nominal: https://github.com/SSProve/ssprove/pull/82

Why do we need them? We don't have them in SSProve. One could potentially add them (but it would be extra work.)

Coq provides native IEEE 754 floats https://drops.dagstuhl.de/opus/volltexte/2019/11062/pdf/LIPIcs-ITP-2019-7.pdf On Wed, Aug 23, 2023 at 11:30 AM Lucas Franceschino < ***@***.***> wrote: > We also had one student here at Inria that...