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 Int63.int 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: Jan 28 2023 at 07:30 UTC