Last change
on this file since 231 was
231,
checked in by mulligan, 10 years ago

BitVector? stuff from this morning: need further development of Nat
theory before I can write any interesting functions on BitVectors?.

File size:
998 bytes

Line  

1  include "Vector.ma". 

2  include "Nat.ma". 

3  include "Bool.ma". 

4  

5  ndefinition BitVector ≝ λn: Nat. Vector Bool n. 

6  ndefinition Bit ≝ BitVector (S Z). 

7  ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). 

8  ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). 

9  ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). 

10  ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 

11  

12  ndefinition zero ≝ 

13  λn: Nat. 

14  replicate Bool n False. 

15  

16  ndefinition conjunction ≝ 

17  λn: Nat. 

18  λb: BitVector n. 

19  λc: BitVector n. 

20  zip Bool Bool Bool n conjunction b c. 

21  

22  ndefinition inclusive_disjunction ≝ 

23  λn: Nat. 

24  λb: BitVector n. 

25  λc: BitVector n. 

26  zip Bool Bool Bool n inclusive_disjunction b c. 

27  

28  ndefinition exclusive_disjunction ≝ 

29  λn: Nat. 

30  λb: BitVector n. 

31  λc: BitVector n. 

32  zip Bool Bool Bool n exclusive_disjunction b c. 

33  

34  nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal n m) ≝ 

35  

Note: See
TracBrowser
for help on using the repository browser.