diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-23 09:50:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-23 09:50:41 +0000 |
| commit | 45954130a813b88bf78e9fd249f92cc05ec5b1b8 (patch) | |
| tree | 6936b022fd0df9bc07b24de19d574acb416a52a8 /test-suite | |
| parent | 9bf1f84def4e7635dd5b81038e5d76ee2a77204e (diff) | |
(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms specs
Currently, 8 lemmas remains to tackle. One proof is done via a _very_
brute-force ugly approach. The all story for proving composition of
phi and phi_inv (and the other way around) is surprisingly long and
tricky. In both cases, comments are welcome, I may have missed an
easier road (?)
As a consequence of the above, we have a additional time-eager
file in the stdlib (about a minute to compile here).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
0 files changed, 0 insertions, 0 deletions