coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] map_eq_nil lemma

From: Michael Day <mikeday AT yeslogic.com>
To: Pierre Casteran <pierre.casteran AT labri.fr>
Cc: Taral <taralx AT gmail.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] map_eq_nil lemma
Date: Thu, 08 Apr 2010 16:44:23 +1000

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

dependent destruction l; auto. ?

A simple case analysis is enough.

Thanks guys, I know it's easy to implement, I just think it should be in the standard library for convenience and consistency :)

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