source: driver/extracted/bindLists.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 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: 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 Option
71
72open Extranat
73
74open Div_and_mod
75
76open Util
77
78open Vector
79
80(** val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list **)
81let bcons e =
82  Obj.magic
83    (Monad.m_map (Monad.max_def Bind_new.bindNew) (fun x -> List.Cons (e,
84      x)))
85
86open Lists
87
Note: See TracBrowser for help on using the repository browser.