source: driver/extracted/jmeq.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: 3.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11type sigma =
12  __
13  (* singleton inductive, whose constructor was mk_Sigma *)
14
15(** val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
16let rec sigma_rect_Type4 h_mk_Sigma x_812 =
17  let x_813 = x_812 in h_mk_Sigma __ x_813
18
19(** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
20let rec sigma_rect_Type5 h_mk_Sigma x_815 =
21  let x_816 = x_815 in h_mk_Sigma __ x_816
22
23(** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
24let rec sigma_rect_Type3 h_mk_Sigma x_818 =
25  let x_819 = x_818 in h_mk_Sigma __ x_819
26
27(** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
28let rec sigma_rect_Type2 h_mk_Sigma x_821 =
29  let x_822 = x_821 in h_mk_Sigma __ x_822
30
31(** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
32let rec sigma_rect_Type1 h_mk_Sigma x_824 =
33  let x_825 = x_824 in h_mk_Sigma __ x_825
34
35(** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
36let rec sigma_rect_Type0 h_mk_Sigma x_827 =
37  let x_828 = x_827 in h_mk_Sigma __ x_828
38
39(** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
40let sigma_inv_rect_Type4 hterm h1 =
41  let hcut = sigma_rect_Type4 h1 hterm in hcut __
42
43(** val sigma_inv_rect_Type3 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
44let sigma_inv_rect_Type3 hterm h1 =
45  let hcut = sigma_rect_Type3 h1 hterm in hcut __
46
47(** val sigma_inv_rect_Type2 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
48let sigma_inv_rect_Type2 hterm h1 =
49  let hcut = sigma_rect_Type2 h1 hterm in hcut __
50
51(** val sigma_inv_rect_Type1 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
52let sigma_inv_rect_Type1 hterm h1 =
53  let hcut = sigma_rect_Type1 h1 hterm in hcut __
54
55(** val sigma_inv_rect_Type0 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
56let sigma_inv_rect_Type0 hterm h1 =
57  let hcut = sigma_rect_Type0 h1 hterm in hcut __
58
59type p1 = __
60
61(** val p2 : sigma -> p1 **)
62let p2 s =
63  let x = s in x
64
65(** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
66let rec jmeq_rect_Type4 x h_refl_jmeq x_851 =
67  h_refl_jmeq
68
69(** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
70let rec jmeq_rect_Type5 x h_refl_jmeq x_854 =
71  h_refl_jmeq
72
73(** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
74let rec jmeq_rect_Type3 x h_refl_jmeq x_857 =
75  h_refl_jmeq
76
77(** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
78let rec jmeq_rect_Type2 x h_refl_jmeq x_860 =
79  h_refl_jmeq
80
81(** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
82let rec jmeq_rect_Type1 x h_refl_jmeq x_863 =
83  h_refl_jmeq
84
85(** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
86let rec jmeq_rect_Type0 x h_refl_jmeq x_866 =
87  h_refl_jmeq
88
89(** val jmeq_inv_rect_Type4 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
90let jmeq_inv_rect_Type4 x2 x4 h1 =
91  let hcut = jmeq_rect_Type4 x2 h1 x4 in hcut __ __
92
93(** val jmeq_inv_rect_Type3 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
94let jmeq_inv_rect_Type3 x2 x4 h1 =
95  let hcut = jmeq_rect_Type3 x2 h1 x4 in hcut __ __
96
97(** val jmeq_inv_rect_Type2 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
98let jmeq_inv_rect_Type2 x2 x4 h1 =
99  let hcut = jmeq_rect_Type2 x2 h1 x4 in hcut __ __
100
101(** val jmeq_inv_rect_Type1 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
102let jmeq_inv_rect_Type1 x2 x4 h1 =
103  let hcut = jmeq_rect_Type1 x2 h1 x4 in hcut __ __
104
105(** val jmeq_inv_rect_Type0 : 'a1 -> 'a2 -> (__ -> __ -> 'a3) -> 'a3 **)
106let jmeq_inv_rect_Type0 x2 x4 h1 =
107  let hcut = jmeq_rect_Type0 x2 h1 x4 in hcut __ __
108
109(** val jmeq_discr : 'a1 -> 'a2 -> __ **)
110let jmeq_discr a2 a4 =
111  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH)) __
112
113(** val cast : 'a1 -> 'a2 **)
114let cast x =
115  (fun x0 -> Obj.magic x0) x
116
117type ('a, 'x) curry = 'x
118
119(** val g : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
120let g x h y =
121  (fun _ -> Logic.eq_rect_Type0 __ h __) __
122
123type 'p pP = 'p
124
125(** val e : 'a1 -> 'a2 pP -> 'a1 -> 'a2 pP **)
126let e a h b =
127  let x = g a h b in x
128
129(** val jmeq_elim : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
130let jmeq_elim x x0 y =
131  e x x0 y
132
Note: See TracBrowser for help on using the repository browser.