Stream: math-comp users

Topic: List utility functions


view this post on Zulip Kimaya Bedarkar (Apr 06 2024 at 11:28):

Hello
I am working with some list manipulation code. I want a list function that does partial lookup.
I found a function in the standard library of Coq that does this:
https://github.com/coq/coq/blob/master/theories/Lists/List.v#L426-L431
As far as I know, there is no equivalent definition in MathComp. I was wondering if this is by design or just an omission.

view this post on Zulip Pierre Roux (Apr 10 2024 at 08:40):

We indeed only have nth that requires a default value and tnth that, in some sense, requires a proof that the index is small enough. I guess we never really felt the need for some nth_opt. Maybe because, for most usecases, you would need to match on the result and then matching on i < size l is probably more or less equivalent.

view this post on Zulip Pierre Roux (Apr 10 2024 at 08:43):

That being said, an addition of some nth_opt with its theory and links with nth would probably be welcome.


Last updated: Jul 15 2024 at 20:02 UTC