source: extracted/bindLists.mli @ 2717

Last change on this file since 2717 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: 516 bytes
Line 
1open Preamble
2
3open State
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Nat
12
13open List
14
15open Setoids
16
17open Relations
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Monad
30
31open Bind_new
32
33type ('b, 'e) bind_list = ('b, 'e List.list) Bind_new.bind_new
34
35val bappend :
36  ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
37
38open Extranat
39
40open Div_and_mod
41
42open Util
43
44open Vector
45
46val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
47
48open Option
49
50open Lists
51
Note: See TracBrowser for help on using the repository browser.