diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-10 16:30:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-10 16:30:44 +0000 |
| commit | afc4f47d56af7d5407acbfd3833527c34eb6e894 (patch) | |
| tree | ac7faa367384a5d14209915ee3116c45214f93b6 /theories/Lists | |
| parent | 7199bf67d9a4eed780e1330ded1644501d2f9872 (diff) | |
Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club
8 April 2010 wish (addition of map_eq_nil).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists')
| -rw-r--r-- | theories/Lists/List.v | 5 | ||||
| -rw-r--r-- | theories/Lists/SetoidList.v | 2 |
2 files changed, 6 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index b3e37685b..766456fff 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -825,6 +825,11 @@ Section Map. rewrite IHl; auto. Qed. + Lemma map_eq_nil : forall l, map l = [] -> l = []. + Proof. + destruct l; simpl; reflexivity || discriminate. + Qed. + (** [flat_map] *) Definition flat_map (f:A -> list B) := diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 2aecb3fdb..d42e71e55 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -489,7 +489,7 @@ left; auto. destruct IHl. left; auto. right; intro; inv; contradiction. -Qed. +Defined. Fixpoint removeA (x : A) (l : list A) : list A := match l with |