Stream: Coq users

Topic: Lemma from library


view this post on Zulip sara lee (Jul 08 2022 at 04:22):

I have taken two lemmas from library . Want to see their proof in the library but i did not find it, where I will look for them?

Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.

  Lemma firstn_length_le: forall l:list A, forall n:nat,  n <= length l -> length (firstn n l) = n.

view this post on Zulip Jiahong Lee (Jul 08 2022 at 04:46):

Use search engine. Or look into the Coq git repo where the stdlib is defined.

For your specific lemmas, they're here.

view this post on Zulip sara lee (Jul 08 2022 at 07:37):

Ok,thank you.


Last updated: Feb 01 2023 at 12:30 UTC