aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/ZModulo/ZModulo.v
AgeCommit message (Collapse)Author
2008-06-01Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inletouzey
a Coq meeting some time ago. NB: this syntax is an alias for (x,(y,(z,t))) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11033 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are letouzey
now dumb wrappers around Zsqrt_plain. Wanted (dead or alive): better implemntations _and_ their proofs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11013 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28CyclicAxioms: after discussion with Laurent, znz_WW and variants areletouzey
transformed into generic functions, and aren't anymore fields of records znz_op/znz_spec. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11012 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
This isn't useful for BigN et BigZ, but it can't hurt; and moreover it's a simple way to understand CyclicAxioms. Next step: proving that Int31 is also an implementation of CyclicAxiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10942 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 14:19:41 +0000