Stream: math-comp devs

Topic: `find` trivial cases


view this post on Zulip Pierre Jouvelot (Apr 01 2023 at 19:59):

I was surprised not to find (sic) the following two limit cases among the other find lemmas:

Lemma findT T (s : seq T) : find xpredT s = 0.
Proof. by elim: s. Qed.

Lemma find0 T (s : seq T) : find xpred0 s = size s.
Proof. by []. Qed.

Have I missed something? If not, shouldn't they be added (or at least the first one) to the seq.v library?

view this post on Zulip Pierre Roux (Apr 04 2023 at 07:20):

Indeed, that looks worth a pull request to add them.


Last updated: Oct 13 2024 at 01:02 UTC