source: extracted/bitVector.mli @ 2746

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

...

File size: 1.2 KB
Line 
1open Preamble
2
3open Bool
4
5open Hints_declaration
6
7open Core_notation
8
9open Pts
10
11open Logic
12
13open Relations
14
15open Nat
16
17open Div_and_mod
18
19open Jmeq
20
21open Russell
22
23open Types
24
25open List
26
27open Util
28
29open FoldStuff
30
31open Extranat
32
33open Vector
34
35type bitVector = Bool.bool Vector.vector
36
37type bit = Bool.bool
38
39type nibble = bitVector
40
41type byte7 = bitVector
42
43type byte = bitVector
44
45type word = bitVector
46
47type word11 = bitVector
48
49val zero : Nat.nat -> bitVector
50
51val maximum : Nat.nat -> bitVector
52
53val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector
54
55val nat_to_bv : Nat.nat -> Nat.nat -> bitVector
56
57val bv_to_nat : Nat.nat -> bitVector -> Nat.nat
58
59val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
60
61val inclusive_disjunction_bv :
62  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
63
64val exclusive_disjunction_bv :
65  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
66
67val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector
68
69val eq_b : Bool.bool -> Bool.bool -> Bool.bool
70
71val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool
72
73val eq_bv_elim :
74  Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
75
Note: See TracBrowser for help on using the repository browser.