include "basics/list.ma".

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

definition assoc_list_add ≝
  λA, B.
  λel: A × B.
  λal: assoc_list A B.
    el :: al.

let rec assoc_list_exists (A: Type[0]) (B: Type[0]) (a: A)
                          (eq: A → A → bool) (al: assoc_list A B) on al ≝
  match al with
  [ nil ⇒ false
  | cons hd tl ⇒
    orb (eq (fst … hd) a) (assoc_list_exists A B a eq tl)
  ].

let rec assoc_list_lookup (A: Type[0]) (B: Type[0]) (a: A)
                          (eq: A → A → bool) (al: assoc_list A B) on al ≝
  match al with
  [ nil        ⇒ None ?
  | cons hd tl ⇒
    match eq (fst ? ? hd) a with
    [ true  ⇒ Some ? (snd … hd)
    | false ⇒ assoc_list_lookup A B a eq tl
    ]
  ].