open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

type ('a, 'b) assoc_list = ('a, 'b) Types.prod List.list

(** val assoc_list_add :
    ('a1, 'a2) Types.prod -> ('a1, 'a2) assoc_list -> ('a1, 'a2) Types.prod
    List.list **)
let assoc_list_add el al =
  List.Cons (el, al)

(** val assoc_list_exists :
    'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
    Bool.bool **)
let rec assoc_list_exists a eq = function
| List.Nil -> Bool.False
| List.Cons (hd, tl) ->
  Bool.orb (eq hd.Types.fst a) (assoc_list_exists a eq tl)

(** val assoc_list_lookup :
    'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
    'a2 Types.option **)
let rec assoc_list_lookup a eq = function
| List.Nil -> Types.None
| List.Cons (hd, tl) ->
  (match eq hd.Types.fst a with
   | Bool.True -> Types.Some hd.Types.snd
   | Bool.False -> assoc_list_lookup a eq tl)