aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic
AgeCommit message (Expand)Author
2008-05-26Cyclic31: cleanup, 2 Admitted killed (6 remaining)letouzey
2008-05-23Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...letouzey
2008-05-23(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...letouzey
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good id...letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum pa...letouzey
2008-05-19Minor improvement: group stuff about carry apart from stuff about zn2zletouzey
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
2008-05-16Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateletouzey
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
2008-05-16ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.letouzey
2008-05-16More BigNum cleanup: letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 1: moving filesletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:38:24 +0000