Last change
on this file since 232 was
232,
checked in by mulligan, 9 years ago

Lots of work from today. Writing bitvector library is harder than it
looks. Not quite sure what Matita has done with `pad'?

File size:
1.1 KB

Rev  Line  

[228]  1  include "Vector.ma". 

 2  include "Nat.ma". 

 3  include "Bool.ma". 

[224]  4  

[228]  5  ndefinition BitVector ≝ λn: Nat. Vector Bool n. 

[230]  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)))))))))))))))). 

[224]  11  

[228]  12  ndefinition zero ≝ 

 13  λn: Nat. 

 14  replicate Bool n False. 

 15  

[224]  16  ndefinition conjunction ≝ 

[228]  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. 

[231]  32  zip Bool Bool Bool n exclusive_disjunction b c. 

 33  

[232]  34  nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝ 

 35  match m with 

 36  [ Z ⇒ ? 

 37   S o ⇒ ? 

 38  ]. 

 39  

 40  //. 

 41  nqed. 

 42  

 43  ncheck pad. 

[231]  44  

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