1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: LegacyField_Compl.v 9273 2006-10-25 11:30:36Z barras $ *)
13
Definition assoc_2nd :=
14
(fix assoc_2nd_rec (A:Type) (B:Set)
15
(eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
16
(lst:list (prod A B)) {struct lst} :
18
fun (key:B) (default:A) =>
22
match eq_dec e key with
24
| right _ => assoc_2nd_rec A B eq_dec l key default
29
(fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2})
30
(a:A) (l:list A) {struct l} : bool :=
34
match eq_dec a a1 with
36
| right _ => mem A eq_dec a l1