source: extracted/bitVector.mli @ 2773

Last change on this file since 2773 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: 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 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 nat_to_bv : Nat.nat -> Nat.nat -> bitVector
62
63val bv_to_nat : Nat.nat -> bitVector -> Nat.nat
64
65val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector
66
67val inclusive_disjunction_bv :
68  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
69
70val exclusive_disjunction_bv :
71  Nat.nat -> bitVector -> bitVector -> Bool.bool Vector.vector
72
73val negation_bv : Nat.nat -> bitVector -> Bool.bool Vector.vector
74
75val eq_b : Bool.bool -> Bool.bool -> Bool.bool
76
77val eq_bv : Nat.nat -> bitVector -> bitVector -> Bool.bool
78
79val eq_bv_elim :
80  Nat.nat -> bitVector -> bitVector -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
81
Note: See TracBrowser for help on using the repository browser.