source: driver/extracted/bindLists.mli @ 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.1 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
35val dpi1__o__blist_from_list__o__inject :
36  ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list) Bind_new.bind_new
37  Types.sig0
38
39val eject__o__blist_from_list__o__inject :
40  'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
41  Types.sig0
42
43val blist_from_list__o__inject :
44  'a2 List.list -> ('a1, 'a2 List.list) Bind_new.bind_new Types.sig0
45
46val dpi1__o__blist_from_list :
47  ('a2 List.list, 'a3) Types.dPair -> ('a1, 'a2 List.list) Bind_new.bind_new
48
49val eject__o__blist_from_list :
50  'a2 List.list Types.sig0 -> ('a1, 'a2 List.list) Bind_new.bind_new
51
52val bappend :
53  ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
54
55open Option
56
57open Extranat
58
59open Div_and_mod
60
61open Util
62
63open Vector
64
65val bcons : 'a2 -> ('a1, 'a2) bind_list -> ('a1, 'a2) bind_list
66
67open Lists
68
Note: See TracBrowser for help on using the repository browser.