source: driver/extracted/bitVectorZ.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 743 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 Setoids
24
25open Monad
26
27open Option
28
29open Extranat
30
31open Vector
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open List
40
41open Util
42
43open FoldStuff
44
45open BitVector
46
47open Exp
48
49open Arithmetic
50
51open Division
52
53val z_of_unsigned_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
54
55val z_of_signed_bitvector : Nat.nat -> BitVector.bitVector -> Z.z
56
57val bits_of_pos : Positive.pos -> Bool.bool List.list
58
59val zeroext_reversed :
60  Nat.nat -> Nat.nat -> BitVector.bitVector -> BitVector.bitVector
61
62val bitvector_of_Z : Nat.nat -> Z.z -> BitVector.bitVector
63
64val pos_length : Positive.pos -> Nat.nat
65
Note: See TracBrowser for help on using the repository browser.