include "ERTL/ERTL.ma".

let rec assoc_list_find
  (A: Type[0]) (B: Type[0]) (eq_a: A → A → bool) (to_find: A)
  (def: B) (l: list (A × B))
    on l ≝
  match l with
  [ nil ⇒ def
  | cons hd tl ⇒
    if eq_a (\fst hd) to_find then
      \snd hd
    else
      assoc_list_find A B eq_a to_find def tl
  ].
      
definition lookup ≝
  λuses.
  λr.
    assoc_list_find register nat (eq_identifier ?) uses 0 r.