source: driver/extracted/setoids.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: 2.3 KB
Line 
1open Preamble
2
3open Core_notation
4
5open Pts
6
7open Hints_declaration
8
9open Logic
10
11open Types
12
13open Relations
14
15type setoid =
16| Mk_Setoid
17
18(** val setoid_rect_Type4 :
19    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
20let rec setoid_rect_Type4 h_mk_Setoid = function
21| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
22
23(** val setoid_rect_Type5 :
24    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
25let rec setoid_rect_Type5 h_mk_Setoid = function
26| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
27
28(** val setoid_rect_Type3 :
29    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
30let rec setoid_rect_Type3 h_mk_Setoid = function
31| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
32
33(** val setoid_rect_Type2 :
34    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
35let rec setoid_rect_Type2 h_mk_Setoid = function
36| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
37
38(** val setoid_rect_Type1 :
39    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
40let rec setoid_rect_Type1 h_mk_Setoid = function
41| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
42
43(** val setoid_rect_Type0 :
44    (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1 **)
45let rec setoid_rect_Type0 h_mk_Setoid = function
46| Mk_Setoid -> h_mk_Setoid __ __ __ __ __
47
48type std_supp = __
49
50(** val setoid_inv_rect_Type4 :
51    setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
52let 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 **)
57let 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 **)
62let 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 **)
67let 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 **)
72let setoid_inv_rect_Type0 hterm h1 =
73  let hcut = setoid_rect_Type0 h1 hterm in hcut __
74
75(** val as_std : setoid **)
76let as_std =
77  Mk_Setoid
78
79(** val std_prod : setoid -> setoid -> setoid **)
80let std_prod x y =
81  Mk_Setoid
82
83(** val std_union : setoid -> setoid -> setoid **)
84let std_union x y =
85  Mk_Setoid
86
Note: See TracBrowser for help on using the repository browser.