source: driver/extracted/setoids.mli @ 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: 1.2 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
18val setoid_rect_Type4 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
19
20val setoid_rect_Type5 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
21
22val setoid_rect_Type3 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
23
24val setoid_rect_Type2 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
25
26val setoid_rect_Type1 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
27
28val setoid_rect_Type0 : (__ -> __ -> __ -> __ -> __ -> 'a1) -> setoid -> 'a1
29
30type std_supp
31
32val setoid_inv_rect_Type4 :
33  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
34
35val setoid_inv_rect_Type3 :
36  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
37
38val setoid_inv_rect_Type2 :
39  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
40
41val setoid_inv_rect_Type1 :
42  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
43
44val setoid_inv_rect_Type0 :
45  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
46
47val as_std : setoid
48
49val std_prod : setoid -> setoid -> setoid
50
51val std_union : setoid -> setoid -> setoid
52
Note: See TracBrowser for help on using the repository browser.