source: src/common/AssocList.ma @ 2540

Last change on this file since 2540 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

File size: 767 bytes
Line 
1include "basics/lists/list.ma".
2
3definition assoc_list ≝ λA, B. list (A × B).
4
5definition assoc_list_add ≝
6  λA, B.
7  λel: A × B.
8  λal: assoc_list A B.
9    el :: al.
10
11let rec assoc_list_exists (A: Type[0]) (B: Type[0]) (a: A)
12                          (eq: A → A → bool) (al: assoc_list A B) on al ≝
13  match al with
14  [ nil ⇒ false
15  | cons hd tl ⇒
16    orb (eq (fst … hd) a) (assoc_list_exists A B a eq tl)
17  ].
18
19let rec assoc_list_lookup (A: Type[0]) (B: Type[0]) (a: A)
20                          (eq: A → A → bool) (al: assoc_list A B) on al ≝
21  match al with
22  [ nil        ⇒ None ?
23  | cons hd tl ⇒
24    match eq (fst ? ? hd) a with
25    [ true  ⇒ Some ? (snd … hd)
26    | false ⇒ assoc_list_lookup A B a eq tl
27    ]
28  ].
29   
Note: See TracBrowser for help on using the repository browser.