|
Last change
on this file since 1624 was
1599,
checked in by sacerdot, 9 years ago
|
|
Start of merging of stuff into the standard library of Matita.
|
|
File size:
767 bytes
|
| Rev | Line | |
|---|
| [1599] | 1 | include "basics/lists/list.ma". |
|---|
| [789] | 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 | ]. |
|---|
| [1599] | 29 | |
|---|
Note: See
TracBrowser
for help on using the repository browser.
