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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size:
602 bytes

Line  

1  include "Vector.ma". 

2  include "Nat.ma". 

3  include "Bool.ma". 

4  

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

6  

7  ndefinition zero ≝ 

8  λn: Nat. 

9  replicate Bool n False. 

10  

11  ndefinition conjunction ≝ 

12  λn: Nat. 

13  λb: BitVector n. 

14  λc: BitVector n. 

15  zip Bool Bool Bool n conjunction b c. 

16  

17  ndefinition inclusive_disjunction ≝ 

18  λn: Nat. 

19  λb: BitVector n. 

20  λc: BitVector n. 

21  zip Bool Bool Bool n inclusive_disjunction b c. 

22  

23  ndefinition exclusive_disjunction ≝ 

24  λn: Nat. 

25  λb: BitVector n. 

26  λc: BitVector n. 

27  zip Bool Bool Bool n exclusive_disjunction b c. 

28  

29  

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