source: driver/extracted/positiveMap.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: 4.0 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31open Setoids
32
33open Monad
34
35open Option
36
37type 'a positive_map =
38| Pm_leaf
39| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
40
41val positive_map_rect_Type4 :
42  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
43  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
44
45val positive_map_rect_Type3 :
46  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
47  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
48
49val positive_map_rect_Type2 :
50  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
51  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
52
53val positive_map_rect_Type1 :
54  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
55  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
56
57val positive_map_rect_Type0 :
58  'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
59  'a2 -> 'a2) -> 'a1 positive_map -> 'a2
60
61val positive_map_inv_rect_Type4 :
62  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
63  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
64
65val positive_map_inv_rect_Type3 :
66  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
67  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
68
69val positive_map_inv_rect_Type2 :
70  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
71  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
72
73val positive_map_inv_rect_Type1 :
74  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
75  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
76
77val positive_map_inv_rect_Type0 :
78  'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
79  'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
80
81val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __
82
83val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __
84
85val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option
86
87val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1
88
89val pm_set :
90  Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map
91
92val insert : Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map
93
94val update :
95  Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option
96
97val fold :
98  (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2
99
100val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map
101
102val is_none : 'a1 Types.option -> Bool.bool
103
104val is_pm_leaf : 'a1 positive_map -> Bool.bool
105
106val map_opt :
107  ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map
108
109val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map
110
111val merge :
112  ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
113  positive_map -> 'a2 positive_map -> 'a3 positive_map
114
115val domain_size : 'a1 positive_map -> Nat.nat
116
117val pm_all_aux :
118  'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
119  (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
120
121val pm_all :
122  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
123
124val pm_choose :
125  'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
126  Types.prod Types.option
127
128val pm_try_remove :
129  Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
130  Types.option
131
132val pm_fold_inf_aux :
133  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
134  positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2
135
136val pm_fold_inf :
137  'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
138
139val pm_find_aux :
140  (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos -> 'a1
141  -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option
142
143val pm_find :
144  'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
145  'a1) Types.prod Types.option
146
Note: See TracBrowser for help on using the repository browser.