source: extracted/bindLists.ml @ 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: 761 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
35(** val bappend :
36    ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
37let bappend x =
38  Obj.magic
39    (Monad.m_bin_op (Monad.max_def Bind_new.bindNew) List.append
40      (Obj.magic x))
41
42open Extranat
43
44open Div_and_mod
45
46open Util
47
48open Vector
49
50(** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
51let bcons e0 =
52  Obj.magic
53    (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e0,
54      x)))
55
56open Option
57
58open Lists
59
Note: See TracBrowser for help on using the repository browser.