1 | open Preamble |
---|
2 | |
---|
3 | open Core_notation |
---|
4 | |
---|
5 | open Pts |
---|
6 | |
---|
7 | open Hints_declaration |
---|
8 | |
---|
9 | open Logic |
---|
10 | |
---|
11 | open Types |
---|
12 | |
---|
13 | open Relations |
---|
14 | |
---|
15 | type setoid = |
---|
16 | | Mk_Setoid |
---|
17 | |
---|
18 | (** val setoid_rect_Type4 : |
---|
19 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
20 | let rec setoid_rect_Type4 h_mk_Setoid = function |
---|
21 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
22 | |
---|
23 | (** val setoid_rect_Type5 : |
---|
24 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
25 | let rec setoid_rect_Type5 h_mk_Setoid = function |
---|
26 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
27 | |
---|
28 | (** val setoid_rect_Type3 : |
---|
29 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
30 | let rec setoid_rect_Type3 h_mk_Setoid = function |
---|
31 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
32 | |
---|
33 | (** val setoid_rect_Type2 : |
---|
34 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
35 | let rec setoid_rect_Type2 h_mk_Setoid = function |
---|
36 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
37 | |
---|
38 | (** val setoid_rect_Type1 : |
---|
39 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
40 | let rec setoid_rect_Type1 h_mk_Setoid = function |
---|
41 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
42 | |
---|
43 | (** val setoid_rect_Type0 : |
---|
44 | (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **) |
---|
45 | let rec setoid_rect_Type0 h_mk_Setoid = function |
---|
46 | | Mk_Setoid -> h_mk_Setoid __ __ __ __ __ |
---|
47 | |
---|
48 | type std_supp = __ |
---|
49 | |
---|
50 | (** val setoid_inv_rect_Type4 : |
---|
51 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
52 | let setoid_inv_rect_Type4 hterm h1 = |
---|
53 | let hcut = setoid_rect_Type4 h1 hterm in hcut __ |
---|
54 | |
---|
55 | (** val setoid_inv_rect_Type3 : |
---|
56 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
57 | let setoid_inv_rect_Type3 hterm h1 = |
---|
58 | let hcut = setoid_rect_Type3 h1 hterm in hcut __ |
---|
59 | |
---|
60 | (** val setoid_inv_rect_Type2 : |
---|
61 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
62 | let setoid_inv_rect_Type2 hterm h1 = |
---|
63 | let hcut = setoid_rect_Type2 h1 hterm in hcut __ |
---|
64 | |
---|
65 | (** val setoid_inv_rect_Type1 : |
---|
66 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
67 | let setoid_inv_rect_Type1 hterm h1 = |
---|
68 | let hcut = setoid_rect_Type1 h1 hterm in hcut __ |
---|
69 | |
---|
70 | (** val setoid_inv_rect_Type0 : |
---|
71 | setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
72 | let setoid_inv_rect_Type0 hterm h1 = |
---|
73 | let hcut = setoid_rect_Type0 h1 hterm in hcut __ |
---|
74 | |
---|
75 | (** val as_std : setoid **) |
---|
76 | let as_std = |
---|
77 | Mk_Setoid |
---|
78 | |
---|
79 | (** val std_prod : setoid -> setoid -> setoid **) |
---|
80 | let std_prod x y = |
---|
81 | Mk_Setoid |
---|
82 | |
---|
83 | (** val std_union : setoid -> setoid -> setoid **) |
---|
84 | let std_union x y = |
---|
85 | Mk_Setoid |
---|
86 | |
---|