source: driver/extracted/nat.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.2 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13type nat =
14| O
15| S of nat
16
17val nat_rect_Type4 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
18
19val nat_rect_Type3 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
20
21val nat_rect_Type2 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
22
23val nat_rect_Type1 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
24
25val nat_rect_Type0 : 'a1 -> (nat -> 'a1 -> 'a1) -> nat -> 'a1
26
27val nat_inv_rect_Type4 :
28  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
29
30val nat_inv_rect_Type3 :
31  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
32
33val nat_inv_rect_Type2 :
34  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
35
36val nat_inv_rect_Type1 :
37  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
38
39val nat_inv_rect_Type0 :
40  nat -> (__ -> 'a1) -> (nat -> (__ -> 'a1) -> __ -> 'a1) -> 'a1
41
42val nat_discr : nat -> nat -> __
43
44val pred : nat -> nat
45
46val plus : nat -> nat -> nat
47
48val times : nat -> nat -> nat
49
50val minus : nat -> nat -> nat
51
52open Bool
53
54val eqb : nat -> nat -> Bool.bool
55
56val leb : nat -> nat -> Bool.bool
57
58val min : nat -> nat -> nat
59
60val max : nat -> nat -> nat
61
Note: See TracBrowser for help on using the repository browser.