source: driver/extracted/div_and_mod.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.5 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
18
19val mod0 : Nat.nat -> Nat.nat -> Nat.nat
20
21val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat
22
23val div : Nat.nat -> Nat.nat -> Nat.nat
24
25val div_mod_spec_rect_Type4 :
26  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
27
28val div_mod_spec_rect_Type5 :
29  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
30
31val div_mod_spec_rect_Type3 :
32  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
33
34val div_mod_spec_rect_Type2 :
35  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
36
37val div_mod_spec_rect_Type1 :
38  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
39
40val div_mod_spec_rect_Type0 :
41  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1
42
43val div_mod_spec_inv_rect_Type4 :
44  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
45
46val div_mod_spec_inv_rect_Type3 :
47  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
48
49val div_mod_spec_inv_rect_Type2 :
50  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
51
52val div_mod_spec_inv_rect_Type1 :
53  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
54
55val div_mod_spec_inv_rect_Type0 :
56  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) -> 'a1
57
58val div_mod_spec_discr : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __
59
Note: See TracBrowser for help on using the repository browser.