Quentin Canu (Dec 02 2021 at 15:52): Quentin Canu (Dec 02 2021 at 15:52):Hello everyone
I am looking for a good way to make iterations on Int63.int integers (using module Int63), is there an elegant way to do so ? Without declaring any nat or lists ?
Pierre Roux (Dec 02 2021 at 16:41):I don't see any, I would probably go through positive using Pos.iter.
Maxime Dénès (Dec 02 2021 at 22:48):Hi! We had some ideas on how to add native iterators based on a computational interpretation of the well foundedness predicate. IIRC it was a suggestion by @Guillaume Melquiond when Int63 were being merged. However, it will require some more work. Meanwhile indeed, going through positives is probably the easiest solution.
Last updated: Sep 30 2023 at 07:01 UTC