source: extracted/extranat.ml @ 2773

Last change on this file since 2773 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: 6.1 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 Jmeq
20
21open Russell
22
23open List
24
25open Setoids
26
27open Monad
28
29open Option
30
31(** val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option **)
32let rec nat_bound_opt n n0 =
33  match n with
34  | Nat.O -> Types.None
35  | Nat.S n' ->
36    (match n0 with
37     | Nat.O -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) __)
38     | Nat.S n'0 ->
39       Obj.magic
40         (Monad.m_bind0 (Monad.max_def Option.option)
41           (Obj.magic (nat_bound_opt n' n'0)) (fun _ ->
42           Monad.m_return0 (Monad.max_def Option.option) __)))
43
44type nat_compared =
45| Nat_lt of Nat.nat * Nat.nat
46| Nat_eq of Nat.nat
47| Nat_gt of Nat.nat * Nat.nat
48
49(** val nat_compared_rect_Type4 :
50    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
51    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
52let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1684 x_1683 = function
53| Nat_lt (n, m) -> h_nat_lt n m
54| Nat_eq n -> h_nat_eq n
55| Nat_gt (n, m) -> h_nat_gt n m
56
57(** val nat_compared_rect_Type5 :
58    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
59    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
60let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1690 x_1689 = function
61| Nat_lt (n, m) -> h_nat_lt n m
62| Nat_eq n -> h_nat_eq n
63| Nat_gt (n, m) -> h_nat_gt n m
64
65(** val nat_compared_rect_Type3 :
66    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
67    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
68let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1696 x_1695 = function
69| Nat_lt (n, m) -> h_nat_lt n m
70| Nat_eq n -> h_nat_eq n
71| Nat_gt (n, m) -> h_nat_gt n m
72
73(** val nat_compared_rect_Type2 :
74    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
75    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
76let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1702 x_1701 = function
77| Nat_lt (n, m) -> h_nat_lt n m
78| Nat_eq n -> h_nat_eq n
79| Nat_gt (n, m) -> h_nat_gt n m
80
81(** val nat_compared_rect_Type1 :
82    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
83    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
84let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1708 x_1707 = function
85| Nat_lt (n, m) -> h_nat_lt n m
86| Nat_eq n -> h_nat_eq n
87| Nat_gt (n, m) -> h_nat_gt n m
88
89(** val nat_compared_rect_Type0 :
90    (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
91    'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
92let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1714 x_1713 = function
93| Nat_lt (n, m) -> h_nat_lt n m
94| Nat_eq n -> h_nat_eq n
95| Nat_gt (n, m) -> h_nat_gt n m
96
97(** val nat_compared_inv_rect_Type4 :
98    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
99    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
100    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
101let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
102  let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __ __
103
104(** val nat_compared_inv_rect_Type3 :
105    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
106    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
107    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
108let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
109  let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __ __
110
111(** val nat_compared_inv_rect_Type2 :
112    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
113    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
114    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
115let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
116  let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __ __
117
118(** val nat_compared_inv_rect_Type1 :
119    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
120    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
121    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
122let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
123  let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __ __
124
125(** val nat_compared_inv_rect_Type0 :
126    Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
127    __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
128    -> __ -> __ -> __ -> 'a1) -> 'a1 **)
129let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
130  let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __ __
131
132(** val nat_compared_discr :
133    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
134let nat_compared_discr a1 a2 x y =
135  Logic.eq_rect_Type2 x
136    (match x with
137     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
138     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
139     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
140
141(** val nat_compared_jmdiscr :
142    Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
143let nat_compared_jmdiscr a1 a2 x y =
144  Logic.eq_rect_Type2 x
145    (match x with
146     | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
147     | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
148     | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
149
150(** val nat_compare : Nat.nat -> Nat.nat -> nat_compared **)
151let rec nat_compare n m =
152  match n with
153  | Nat.O ->
154    (match m with
155     | Nat.O -> Nat_eq Nat.O
156     | Nat.S m' -> Nat_lt (Nat.O, m'))
157  | Nat.S n' ->
158    (match m with
159     | Nat.O -> Nat_gt (n', Nat.O)
160     | Nat.S m' ->
161       (match nat_compare n' m' with
162        | Nat_lt (x, y) -> Nat_lt ((Nat.S x), y)
163        | Nat_eq x -> Nat_eq (Nat.S x)
164        | Nat_gt (x, y) -> Nat_gt (x, (Nat.S y))))
165
166(** val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum **)
167let rec eq_nat_dec n m =
168  match n with
169  | Nat.O ->
170    (match m with
171     | Nat.O -> Types.Inl __
172     | Nat.S m' -> Types.Inr __)
173  | Nat.S n' ->
174    (match m with
175     | Nat.O -> Types.Inr __
176     | Nat.S m' ->
177       (match eq_nat_dec n' m' with
178        | Types.Inl _ -> Types.Inl __
179        | Types.Inr _ -> Types.Inr __))
180
Note: See TracBrowser for help on using the repository browser.