Changeset 281 for Deliverables/D4.1/Matita/Arithmetic.ma
 Timestamp:
 Nov 24, 2010, 6:29:12 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r277 r281 27 27 ndefinition eighteen ≝ nine + nine. 28 28 ndefinition nineteen ≝ ten + nine. 29 ndefinition one_hundred ≝ ten * ten. 29 30 ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. 31 ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one. 32 ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one. 33 ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one. 34 ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven. 35 ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one. 36 ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one. 37 ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten. 38 ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one. 39 ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one. 40 ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one. 41 ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen. 42 ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight. 43 ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine. 44 ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen. 45 ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight. 46 ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen. 47 ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight. 48 ndefinition two_hundred ≝ one_hundred + one_hundred. 49 ndefinition two_hundred_and_two ≝ two_hundred + two. 50 ndefinition two_hundred_and_three ≝ two_hundred_and_two + one. 51 ndefinition two_hundred_and_four ≝ two_hundred_and_three + one. 52 ndefinition two_hundred_and_five ≝ two_hundred_and_four + one. 53 ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three. 54 ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen. 55 ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen. 30 56 ndefinition two_hundred_and_fifty_six ≝ 31 one_hundred_and_twenty_eight + one_hundred_and_twenty_eight. 57 one_hundred_and_twenty_eight + one_hundred_and_twenty_eight. 32 58 33 59 ndefinition nat_of_bool ≝
Note: See TracChangeset
for help on using the changeset viewer.