Last change
on this file since 228 was
228,
checked in by mulligan, 9 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.