source: extracted/utilBranch.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 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
Line 
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
29open Exp
30
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.