source: extracted/bitVectorZ.mli @ 2717

Last change on this file since 2717 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: 704 bytes
Line 
1open Preamble
2
3open Types
4
5open Bool
6
7open Relations
8
9open Nat
10
11open Hints_declaration
12
13open Core_notation
14
15open Pts
16
17open Logic
18
19open Positive
20
21open Z
22
23open Extranat
24
25open Vector
26
27open Div_and_mod
28
29open Jmeq
30
31open Russell
32
33open List
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Exp
42
43open Arithmetic
44
45open Division
46
47val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
48
49val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
50
51val bits_of_pos : Positive.pos -> Bool.bool List.list
52
53val zeroext_reversed :
54  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
55
56val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
57
58val pos_length : Positive.pos -> Nat.nat
59
Note: See TracBrowser for help on using the repository browser.