From bdc7b815d033f84e5538a1c8db87d3c061b1ca4c Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 5 Aug 2009 14:40:34 +0000 Subject: Added 'going wrong' behaviors git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Coqlib.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'lib/Coqlib.v') 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. *) -- cgit