Last change
on this file since 1517 was
789,
checked in by mulligan, 10 years ago

More work on rtlabs > rtl pass.

File size:
760 bytes

Line  

1  include "basics/list.ma". 

2  

3  definition assoc_list ≝ λA, B. list (A × B). 

4  

5  definition assoc_list_add ≝ 

6  λA, B. 

7  λel: A × B. 

8  λal: assoc_list A B. 

9  el :: al. 

10  

11  let 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  

19  let 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.