1 | open Preamble |
---|
2 | |
---|
3 | open Hints_declaration |
---|
4 | |
---|
5 | open Core_notation |
---|
6 | |
---|
7 | open Pts |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Types |
---|
12 | |
---|
13 | type order = |
---|
14 | | Order_lt |
---|
15 | | Order_eq |
---|
16 | | Order_gt |
---|
17 | |
---|
18 | (** val order_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
19 | let rec order_rect_Type4 h_order_lt h_order_eq h_order_gt = function |
---|
20 | | Order_lt -> h_order_lt |
---|
21 | | Order_eq -> h_order_eq |
---|
22 | | Order_gt -> h_order_gt |
---|
23 | |
---|
24 | (** val order_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
25 | let rec order_rect_Type5 h_order_lt h_order_eq h_order_gt = function |
---|
26 | | Order_lt -> h_order_lt |
---|
27 | | Order_eq -> h_order_eq |
---|
28 | | Order_gt -> h_order_gt |
---|
29 | |
---|
30 | (** val order_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
31 | let rec order_rect_Type3 h_order_lt h_order_eq h_order_gt = function |
---|
32 | | Order_lt -> h_order_lt |
---|
33 | | Order_eq -> h_order_eq |
---|
34 | | Order_gt -> h_order_gt |
---|
35 | |
---|
36 | (** val order_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
37 | let rec order_rect_Type2 h_order_lt h_order_eq h_order_gt = function |
---|
38 | | Order_lt -> h_order_lt |
---|
39 | | Order_eq -> h_order_eq |
---|
40 | | Order_gt -> h_order_gt |
---|
41 | |
---|
42 | (** val order_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
43 | let rec order_rect_Type1 h_order_lt h_order_eq h_order_gt = function |
---|
44 | | Order_lt -> h_order_lt |
---|
45 | | Order_eq -> h_order_eq |
---|
46 | | Order_gt -> h_order_gt |
---|
47 | |
---|
48 | (** val order_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> order -> 'a1 **) |
---|
49 | let rec order_rect_Type0 h_order_lt h_order_eq h_order_gt = function |
---|
50 | | Order_lt -> h_order_lt |
---|
51 | | Order_eq -> h_order_eq |
---|
52 | | Order_gt -> h_order_gt |
---|
53 | |
---|
54 | (** val order_inv_rect_Type4 : |
---|
55 | order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
56 | let order_inv_rect_Type4 hterm h1 h2 h3 = |
---|
57 | let hcut = order_rect_Type4 h1 h2 h3 hterm in hcut __ |
---|
58 | |
---|
59 | (** val order_inv_rect_Type3 : |
---|
60 | order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
61 | let order_inv_rect_Type3 hterm h1 h2 h3 = |
---|
62 | let hcut = order_rect_Type3 h1 h2 h3 hterm in hcut __ |
---|
63 | |
---|
64 | (** val order_inv_rect_Type2 : |
---|
65 | order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
66 | let order_inv_rect_Type2 hterm h1 h2 h3 = |
---|
67 | let hcut = order_rect_Type2 h1 h2 h3 hterm in hcut __ |
---|
68 | |
---|
69 | (** val order_inv_rect_Type1 : |
---|
70 | order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
71 | let order_inv_rect_Type1 hterm h1 h2 h3 = |
---|
72 | let hcut = order_rect_Type1 h1 h2 h3 hterm in hcut __ |
---|
73 | |
---|
74 | (** val order_inv_rect_Type0 : |
---|
75 | order -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
76 | let order_inv_rect_Type0 hterm h1 h2 h3 = |
---|
77 | let hcut = order_rect_Type0 h1 h2 h3 hterm in hcut __ |
---|
78 | |
---|
79 | (** val order_discr : order -> order -> __ **) |
---|
80 | let order_discr x y = |
---|
81 | Logic.eq_rect_Type2 x |
---|
82 | (match x with |
---|
83 | | Order_lt -> Obj.magic (fun _ dH -> dH) |
---|
84 | | Order_eq -> Obj.magic (fun _ dH -> dH) |
---|
85 | | Order_gt -> Obj.magic (fun _ dH -> dH)) y |
---|
86 | |
---|