source: driver/extracted/division.mli @ 3106

Last change on this file since 3106 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.6 KB
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23type natp =
24| Pzero
25| Ppos of Positive.pos
26
27val natp_rect_Type4 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
28
29val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
30
31val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
32
33val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
34
35val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
36
37val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1
38
39val natp_inv_rect_Type4 :
40  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
41
42val natp_inv_rect_Type3 :
43  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
44
45val natp_inv_rect_Type2 :
46  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
47
48val natp_inv_rect_Type1 :
49  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
50
51val natp_inv_rect_Type0 :
52  natp -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> 'a1
53
54val natp_discr : natp -> natp -> __
55
56val natp0 : natp -> natp
57
58val natp1 : natp -> natp
59
60val divide : Positive.pos -> Positive.pos -> (natp, natp) Types.prod
61
62val div : Positive.pos -> Positive.pos -> natp
63
64val mod0 : Positive.pos -> Positive.pos -> natp
65
66val natp_plus : natp -> natp -> natp
67
68val natp_times : natp -> natp -> natp
69
70val dec_divides : Positive.pos -> Positive.pos -> (__, __) Types.sum
71
72val dec_dividesZ : Z.z -> Z.z -> (__, __) Types.sum
73
74val natp_to_Z : natp -> Z.z
75
76val natp_to_negZ : natp -> Z.z
77
78val divZ : Z.z -> Z.z -> Z.z
79
80val modZ : Z.z -> Z.z -> Z.z
81
Note: See TracBrowser for help on using the repository browser.