source: extracted/bitVectorZ.mli @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 694 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 Arithmetic
42
43open Division
44
45val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
46
47val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
48
49val bits_of_pos : Positive.pos -> Bool.bool List.list
50
51val zeroext_reversed :
52  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
53
54val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
55
56val pos_length : Positive.pos -> Nat.nat
57
Note: See TracBrowser for help on using the repository browser.