Stream: Coq users

Topic: Int63 fold

view this post on Zulip Quentin Canu (Dec 02 2021 at 15:52):

Hello everyone

I am looking for a good way to make iterations on integers (using module Int63), is there an elegant way to do so ? Without declaring any nat or lists ?

view this post on Zulip Pierre Roux (Dec 02 2021 at 16:41):

I don't see any, I would probably go through positive using Pos.iter.

view this post on Zulip 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: Jun 20 2024 at 13:02 UTC