source: driver/extracted/bitVector.mli @ 3106

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

Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were
using the wrong indianess. They were also redundant with the good
(but inefficient) ones in Arithmetic.ma.

On a simple test the compiled code runs (I have not checked the
result).

File size: 1.1 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 Setoids
32
33open Monad
34
35open Option
36
37open Extranat
38
39open Vector
40
41type bitVector = Bool.bool Vector.vector
42
43type bit = Bool.bool
44
45type nibble = bitVector
46
47type byte7 = bitVector
48
49type byte = bitVector
50
51type word = bitVector
52
53type word11 = bitVector
54
55val zero : Nat.nat -> bitVector
56
57val maximum : Nat.nat -> bitVector
58
59val pad : Nat.nat -> Nat.nat -> bitVector -> Bool.bool Vector.vector
60
61val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
62
63val inclusive_disjunction_bv :
64  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
65
66val exclusive_disjunction_bv :
67  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
68
69val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector
70
71val eq_b : Bool.bool -> Bool.bool -> Bool.bool
72
73val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool
74
75val eq_bv_elim :
76  Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
77
Note: See TracBrowser for help on using the repository browser.