coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] map_eq_nil lemma

From: Michael Day <mikeday AT yeslogic.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] map_eq_nil lemma
Date: Thu, 08 Apr 2010 14:08:56 +1000

Hi,

Perhaps it would be worth adding a lemma to the List module like this:

map_eq_nil : forall l, map f l = nil -> l = nil.

Similar to app_eq_nil, it's simple but handy sometimes.

Cheers,

Michael

--
Print XML with Prince!
http://www.princexml.com

[Coq-Club] map_eq_nil lemma, Michael Day
- Re: [Coq-Club] map_eq_nil lemma, Taral
  - Re: [Coq-Club] map_eq_nil lemma, Pierre Casteran
    - Re: [Coq-Club] map_eq_nil lemma, Michael Day