source: extracted/deqsets.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.8 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Bool
16
17type deqSet =
18  __ -> __ -> Bool.bool
19  (* singleton inductive, whose constructor was mk_DeqSet *)
20
21val deqSet_rect_Type4 :
22  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
23
24val deqSet_rect_Type5 :
25  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
26
27val deqSet_rect_Type3 :
28  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
29
30val deqSet_rect_Type2 :
31  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
32
33val deqSet_rect_Type1 :
34  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
35
36val deqSet_rect_Type0 :
37  (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1
38
39type carr
40
41val eqb : deqSet -> __ -> __ -> Bool.bool
42
43val deqSet_inv_rect_Type4 :
44  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
45
46val deqSet_inv_rect_Type3 :
47  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
48
49val deqSet_inv_rect_Type2 :
50  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
51
52val deqSet_inv_rect_Type1 :
53  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
54
55val deqSet_inv_rect_Type0 :
56  deqSet -> (__ -> (__ -> __ -> Bool.bool) -> __ -> __ -> 'a1) -> 'a1
57
58val beqb : Bool.bool -> Bool.bool -> Bool.bool
59
60val deqBool : deqSet
61
62val eq_option : deqSet -> __ Types.option -> __ Types.option -> Bool.bool
63
64val deqOption : deqSet -> deqSet
65
66val eq_pairs :
67  deqSet -> deqSet -> (__, __) Types.prod -> (__, __) Types.prod -> Bool.bool
68
69val deqProd : deqSet -> deqSet -> deqSet
70
71val eq_sum :
72  deqSet -> deqSet -> (__, __) Types.sum -> (__, __) Types.sum -> Bool.bool
73
74val deqSum : deqSet -> deqSet -> deqSet
75
76val eq_sigma : deqSet -> __ Types.sig0 -> __ Types.sig0 -> Bool.bool
77
78val deqSig : deqSet -> deqSet
79
Note: See TracBrowser for help on using the repository browser.