source: extracted/assocList.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 8 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 979 bytes
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21type ('a, 'b) assoc_list = ('a, 'b) Types.prod List.list
22
23(** val assoc_list_add :
24    ('a1, 'a2) Types.prod -> ('a1, 'a2) assoc_list -> ('a1, 'a2) Types.prod
25    List.list **)
26let assoc_list_add el al =
27  List.Cons (el, al)
28
29(** val assoc_list_exists :
30    'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
31    Bool.bool **)
32let rec assoc_list_exists a eq = function
33| List.Nil -> Bool.False
34| List.Cons (hd, tl) ->
35  Bool.orb (eq hd.Types.fst a) (assoc_list_exists a eq tl)
36
37(** val assoc_list_lookup :
38    'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
39    'a2 Types.option **)
40let rec assoc_list_lookup a eq = function
41| List.Nil -> Types.None
42| List.Cons (hd, tl) ->
43  (match eq hd.Types.fst a with
44   | Bool.True -> Types.Some hd.Types.snd
45   | Bool.False -> assoc_list_lookup a eq tl)
46
Note: See TracBrowser for help on using the repository browser.