Changeset 257
 Timestamp:
 Nov 23, 2010, 11:43:14 AM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r248 r257 7 7 include "BitVector.ma". 8 8 include "List.ma". 9 10 ndefinition eight ≝ exponential (S(S(Z))) (S(S(S(Z)))). 9 10 ndefinition one ≝ S Z. 11 ndefinition two ≝ (S(S(Z))). 12 ndefinition three ≝ two + one. 13 ndefinition four ≝ two + two. 14 ndefinition five ≝ three + two. 15 ndefinition six ≝ three + three. 16 ndefinition seven ≝ three + four. 17 ndefinition eight ≝ four + four. 18 ndefinition nine ≝ five + four. 19 ndefinition ten ≝ five + five. 20 ndefinition eleven ≝ six + five. 21 ndefinition twelve ≝ six + six. 22 ndefinition thirteen ≝ seven + six. 23 ndefinition fourteen ≝ seven + seven. 24 ndefinition fifteen ≝ eight + seven. 11 25 ndefinition sixteen ≝ eight + eight. 26 ndefinition seventeen ≝ nine + eight. 27 ndefinition eighteen ≝ nine + nine. 28 ndefinition nineteen ≝ ten + nine. 12 29 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. 13 30 ndefinition two_hundred_and_fifty_six ≝ 
Deliverables/D4.1/Matita/BitVector.ma
r248 r257 55 55 ndefinition zero ≝ 56 56 λn: Nat. 57 replicate Bool n False.57 ((replicate Bool n False): BitVector n). 58 58 59 59 ndefinition max ≝ 60 60 λn: Nat. 61 replicate Bool n True.61 ((replicate Bool n True): BitVector n). 62 62 63 63 ndefinition append ≝
Note: See TracChangeset
for help on using the changeset viewer.