diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-05 14:40:34 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-08-05 14:40:34 +0000 |
| commit | bdc7b815d033f84e5538a1c8db87d3c061b1ca4c (patch) | |
| tree | bc3ca91f80b4193335cdcc07e7003c9527b48350 /lib/Coqlib.v | |
| parent | 213bf38509f4f92545d4c5749c25a55b9a9dda36 (diff) | |
| download | compcert-kvx-bdc7b815d033f84e5538a1c8db87d3c061b1ca4c.tar.gz compcert-kvx-bdc7b815d033f84e5538a1c8db87d3c061b1ca4c.zip | |
Added 'going wrong' behaviors
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib/Coqlib.v')
| -rw-r--r-- | lib/Coqlib.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 9e2199c1..416afa9c 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -781,6 +781,11 @@ Proof. right; red; intros. elim n0. eapply list_disjoint_cons_left; eauto. Defined. +(** [list_equiv l1 l2] holds iff the lists [l1] and [l2] contain the same elements. *) + +Definition list_equiv (A : Type) (l1 l2: list A) : Prop := + forall x, In x l1 <-> In x l2. + (** [list_norepet l] holds iff the list [l] contains no repetitions, i.e. no element occurs twice. *) |