source: extracted/setoids.mli @ 2746

Last change on this file since 2746 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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
32type std_eq = __
33
34val setoid_inv_rect_Type4 :
35  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
36
37val setoid_inv_rect_Type3 :
38  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
39
40val setoid_inv_rect_Type2 :
41  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
42
43val setoid_inv_rect_Type1 :
44  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
45
46val setoid_inv_rect_Type0 :
47  setoid -> (__ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
48
49val as_std : setoid
50
51val std_prod : setoid -> setoid -> setoid
52
53val std_union : setoid -> setoid -> setoid
54
Note: See TracBrowser for help on using the repository browser.