source: extracted/z.mli @ 2755

Last change on this file since 2755 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: 2.0 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Positive
18
19type z =
20| OZ
21| Pos of Positive.pos
22| Neg of Positive.pos
23
24val z_rect_Type4 :
25  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
26
27val z_rect_Type5 :
28  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
29
30val z_rect_Type3 :
31  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
32
33val z_rect_Type2 :
34  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
35
36val z_rect_Type1 :
37  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
38
39val z_rect_Type0 :
40  'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1
41
42val z_inv_rect_Type4 :
43  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
44  'a1) -> 'a1
45
46val z_inv_rect_Type3 :
47  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
48  'a1) -> 'a1
49
50val z_inv_rect_Type2 :
51  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
52  'a1) -> 'a1
53
54val z_inv_rect_Type1 :
55  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
56  'a1) -> 'a1
57
58val z_inv_rect_Type0 :
59  z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ ->
60  'a1) -> 'a1
61
62val z_discr : z -> z -> __
63
64val z_of_nat : Nat.nat -> z
65
66val neg_Z_of_nat : Nat.nat -> z
67
68val abs : z -> Nat.nat
69
70val oZ_test : z -> Bool.bool
71
72val zsucc : z -> z
73
74val zpred : z -> z
75
76type zle = __
77
78type zlt = __
79
80val eqZb : z -> z -> Bool.bool
81
82val z_compare : z -> z -> Positive.compare
83
84val zplus : z -> z -> z
85
86val zopp : z -> z
87
88val zminus : z -> z -> z
89
90val z_two_power_nat : Nat.nat -> z
91
92val z_two_power_pos : Positive.pos -> z
93
94val two_p : z -> z
95
96open Types
97
98val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum
99
100val zleb : z -> z -> Bool.bool
101
102val zltb : z -> z -> Bool.bool
103
104val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
105
106val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
107
108val z_times : z -> z -> z
109
110val zmax : z -> z -> z
111
Note: See TracBrowser for help on using the repository browser.