source: driver/extracted/deqsets.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: 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 Relations
14
15open Bool
16
17type deqSet =
18  __ -> __ -> Bool.bool
19  (* singleton inductive, whose constructor was mk_DeqSet *)
20
21(** val deqSet_rect_Type4 :
22    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
23let rec deqSet_rect_Type4 h_mk_DeqSet x_3369 =
24  let eqb = x_3369 in h_mk_DeqSet __ eqb __
25
26(** val deqSet_rect_Type5 :
27    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
28let rec deqSet_rect_Type5 h_mk_DeqSet x_3371 =
29  let eqb = x_3371 in h_mk_DeqSet __ eqb __
30
31(** val deqSet_rect_Type3 :
32    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
33let rec deqSet_rect_Type3 h_mk_DeqSet x_3373 =
34  let eqb = x_3373 in h_mk_DeqSet __ eqb __
35
36(** val deqSet_rect_Type2 :
37    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
38let rec deqSet_rect_Type2 h_mk_DeqSet x_3375 =
39  let eqb = x_3375 in h_mk_DeqSet __ eqb __
40
41(** val deqSet_rect_Type1 :
42    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
43let rec deqSet_rect_Type1 h_mk_DeqSet x_3377 =
44  let eqb = x_3377 in h_mk_DeqSet __ eqb __
45
46(** val deqSet_rect_Type0 :
47    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
48let rec deqSet_rect_Type0 h_mk_DeqSet x_3379 =
49  let eqb = x_3379 in h_mk_DeqSet __ eqb __
50
51type carr = __
52
53(** val eqb : deqSet -> __ -> __ -> Bool.bool **)
54let rec eqb xxx =
55  let yyy = xxx in yyy
56
57(** val deqSet_inv_rect_Type4 :
58    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
59let deqSet_inv_rect_Type4 hterm h1 =
60  let hcut = deqSet_rect_Type4 h1 hterm in hcut __
61
62(** val deqSet_inv_rect_Type3 :
63    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
64let deqSet_inv_rect_Type3 hterm h1 =
65  let hcut = deqSet_rect_Type3 h1 hterm in hcut __
66
67(** val deqSet_inv_rect_Type2 :
68    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
69let deqSet_inv_rect_Type2 hterm h1 =
70  let hcut = deqSet_rect_Type2 h1 hterm in hcut __
71
72(** val deqSet_inv_rect_Type1 :
73    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
74let deqSet_inv_rect_Type1 hterm h1 =
75  let hcut = deqSet_rect_Type1 h1 hterm in hcut __
76
77(** val deqSet_inv_rect_Type0 :
78    deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1 **)
79let deqSet_inv_rect_Type0 hterm h1 =
80  let hcut = deqSet_rect_Type0 h1 hterm in hcut __
81
82(** val beqb : Bool.bool -> Bool.bool -> Bool.bool **)
83let beqb b1 b2 =
84  match b1 with
85  | Bool.True -> b2
86  | Bool.False -> Bool.notb b2
87
88(** val deqBool : deqSet **)
89let deqBool =
90  Obj.magic beqb
91
92(** val eq_option :
93    deqSet -> __ Types.option -> __ Types.option -> Bool.bool **)
94let eq_option a a1 a2 =
95  match a1 with
96  | Types.None ->
97    (match a2 with
98     | Types.None -> Bool.True
99     | Types.Some x -> Bool.False)
100  | Types.Some a1' ->
101    (match a2 with
102     | Types.None -> Bool.False
103     | Types.Some a2' -> eqb a a1' a2')
104
105(** val deqOption : deqSet -> deqSet **)
106let deqOption a =
107  Obj.magic (eq_option a)
108
109(** val eq_pairs :
110    deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod ->
111    Bool.bool **)
112let eq_pairs a b p1 p2 =
113  Bool.andb (eqb a p1.Types.fst p2.Types.fst)
114    (eqb b p1.Types.snd p2.Types.snd)
115
116(** val deqProd : deqSet -> deqSet -> deqSet **)
117let deqProd a b =
118  Obj.magic (eq_pairs a b)
119
120(** val eq_sum :
121    deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool **)
122let eq_sum a b p1 p2 =
123  match p1 with
124  | Types.Inl a1 ->
125    (match p2 with
126     | Types.Inl a2 -> eqb a a1 a2
127     | Types.Inr b2 -> Bool.False)
128  | Types.Inr b1 ->
129    (match p2 with
130     | Types.Inl a2 -> Bool.False
131     | Types.Inr b2 -> eqb b b1 b2)
132
133(** val deqSum : deqSet -> deqSet -> deqSet **)
134let deqSum a b =
135  Obj.magic (eq_sum a b)
136
137(** val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool **)
138let eq_sigma a p1 p2 =
139  let a1 = p1 in let a2 = p2 in eqb a a1 a2
140
141(** val deqSig : deqSet -> deqSet **)
142let deqSig a =
143  Obj.magic (eq_sigma a)
144
Note: See TracBrowser for help on using the repository browser.