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.
https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v#L77
thanks, I was looking in this file and somehow I missed it, thanks!
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.
Why did mathcomp use seq
instead of list
? Why the renaming?
Or maybe seq
is something more than list
?
Check fun l => 1 :: 2 :: 3 :: l.
Infinite sequences possible?
if you want infinite sequences, you'll have to use coinductive types of some form. But infinite sequences are not in MathComp.
Duh.. I guess it isn't infinite. Just prepends 1,2,3 to l
.
Yeah.
Julin Shaji said:
Why did mathcomp use
seq
instead oflist
? Why the renaming?
This is because mathcomp used to redefine list, they have been realigned for a while now, but the renaming never happened.
Ah.. that makes sense.
Last updated: Oct 13 2024 at 01:02 UTC