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.

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.

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