source: extracted/assocList.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 534 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
23val assoc_list_add :
24  ('a1, 'a2) Types.prod -> ('a1, 'a2) assoc_list -> ('a1, 'a2) Types.prod
25  List.list
26
27val assoc_list_exists :
28  'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list ->
29  Bool.bool
30
31val assoc_list_lookup :
32  'a1 -> ('a1 -> 'a1 -> Bool.bool) -> ('a1, 'a2) Types.prod List.list -> 'a2
33  Types.option
34
Note: See TracBrowser for help on using the repository browser.