source: extracted/lists.mli @ 2731

Last change on this file since 2731 was 2601, checked in by sacerdot, 8 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: 964 bytes
RevLine 
[2601]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 Types
18
19open List
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29val all0 : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool
30
31type all2 = __
32
33val map_All : ('a1 -> __ -> 'a2) -> 'a1 List.list -> 'a2 List.list
34
35open Setoids
36
37open Monad
38
39open Option
40
41val append0 : 'a1 List.list List.aop
42
43val list0 : Monad.monadProps
44
45val count : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
46
47val position_of_safe : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
48
49val index_of : ('a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat
50
51val ordered_insert :
52  ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> 'a1 List.list
53
54val insert_sort : ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list
55
56val range_strong_internal :
57  Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat Types.sig0 List.list
58
59val range_strong : Nat.nat -> Nat.nat Types.sig0 List.list
60
Note: See TracBrowser for help on using the repository browser.