Stream: math-comp users

Topic: First element of a seq that fulfil a condition


view this post on Zulip walker (Sep 14 2023 at 08:22):

is there a an already existing function (must be function) that returns the first element of list that fulfill some requirement of none if it fails to?

It is not hard to impelemet, but it if is there, then (at least I hope) there should also be lemmas for how it integrate with everything.

view this post on Zulip Pierre Roux (Sep 14 2023 at 08:34):

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v#L77

view this post on Zulip walker (Sep 14 2023 at 09:17):

thanks, I was looking in this file and somehow I missed it, thanks!

view this post on Zulip Kazuhiko Sakaguchi (Sep 14 2023 at 09:19):

Note that it returns the index of type nat, not the element. But I agree that it is the closest thing to what you are looking for.

view this post on Zulip Julin Shaji (Oct 11 2023 at 05:50):

Why did mathcomp use seq instead of list? Why the renaming?

view this post on Zulip Julin Shaji (Oct 11 2023 at 06:26):

Or maybe seq is something more than list?

Check fun l => 1 :: 2 :: 3 :: l.

view this post on Zulip Julin Shaji (Oct 11 2023 at 06:27):

Infinite sequences possible?

view this post on Zulip Karl Palmskog (Oct 11 2023 at 06:28):

if you want infinite sequences, you'll have to use coinductive types of some form. But infinite sequences are not in MathComp.

view this post on Zulip Julin Shaji (Oct 11 2023 at 06:28):

Duh.. I guess it isn't infinite. Just prepends 1,2,3 to l.

view this post on Zulip Julin Shaji (Oct 11 2023 at 06:29):

Yeah.

view this post on Zulip Cyril Cohen (Oct 11 2023 at 07:44):

Julin Shaji said:

Why did mathcomp use seq instead of list? Why the renaming?

This is because mathcomp used to redefine list, they have been realigned for a while now, but the renaming never happened.

view this post on Zulip Julin Shaji (Oct 11 2023 at 07:44):

Ah.. that makes sense.


Last updated: Jul 25 2024 at 15:02 UTC