source: extracted/utilBranch.mli @ 2731

Last change on this file since 2731 was 2717, checked in by sacerdot, 8 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 323 bytes
RevLine 
[2601]1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
[2717]29open Exp
30
[2601]31open Extranat
32
33open Vector
34
35open FoldStuff
36
37open BitVector
38
39open Arithmetic
40
41val nat_of_bool0 : Bool.bool -> Nat.nat
42
Note: See TracBrowser for help on using the repository browser.