source: extracted/bindLists.ml @ 2743

Last change on this file since 2743 was 2743, checked in by sacerdot, 8 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 1.7 KB
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 dpi1__o__blist_from_list__o__inject :
36    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
37    Bind_new.bind_new Types.sig0 **)
38let dpi1__o__blist_from_list__o__inject x4 =
39  Bind_new.Bret x4.Types.dpi1
40
41(** val eject__o__blist_from_list__o__inject :
42    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
43    Types.sig0 **)
44let eject__o__blist_from_list__o__inject x4 =
45  Bind_new.Bret (Types.pi1 x4)
46
47(** val blist_from_list__o__inject :
48    'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0 **)
49let blist_from_list__o__inject x3 =
50  Bind_new.Bret x3
51
52(** val dpi1__o__blist_from_list :
53    ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list)
54    Bind_new.bind_new **)
55let dpi1__o__blist_from_list x3 =
56  let l = x3.Types.dpi1 in Bind_new.Bret l
57
58(** val eject__o__blist_from_list :
59    'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new **)
60let eject__o__blist_from_list x3 =
61  let l = Types.pi1 x3 in Bind_new.Bret l
62
63(** val bappend :
64    ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
65let bappend x =
66  Obj.magic
67    (Monad.m_bin_op (Monad.max_def Bind_new.bindNew) List.append
68      (Obj.magic x))
69
70open Extranat
71
72open Div_and_mod
73
74open Util
75
76open Vector
77
78(** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
79let bcons e0 =
80  Obj.magic
81    (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e0,
82      x)))
83
84open Option
85
86open Lists
87
Note: See TracBrowser for help on using the repository browser.