| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9883 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Pplus_xO
Pmult_Sn_m
Pcompare_eq_Lt (a generalization of Pcompare_Gt_Lt)
Pcompare_eq_Gt (a generalization of Pcompare_Lt_Gt)
Pcompare_refl_id (a generalization of Pcompare_refl)
Pcompare_Lt_eq_Lt (a generalization of Pcompare_Lt_Lt)
Pcompare_Gt_eq_Gt (a generalization of Pcompare_Gt_Gt)
Pcompare_p_Sp
Pcompare_p_Sq (one of the defining axioms of < )
Pcompare_1 (1 is the least positive number)
Added the following theorems to BinNat:
Nrect (defined in terms of new Prect)
Nrect_base
Nrect_step (the analogout statement in BinPos is called Prect_succ)
Nrec_base
Nrec_step
Nmult_Sn_m
Nsucc_0
Ncompare_0 (0 is the least natural number)
Ncompare_n_Sm (one of the defining axioms of < )
Also, defined Nind and Nrec in terms of Nrect.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9738 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8771 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* le type ad des adresses est maintenant un alias vers
le N de NArith, qui lui est isomorphe.
* toutes les operations sur ces adresses (p.ex. un xor
bit a bit) sont maintenant dans de nouveaux fichiers du
repertoire NArith.
* Intmap utilise maintenant le meme type option que le
reste du monde
* etc etc...
Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs
utilisant Intmap sont adaptees en consequence. Me demander si besoin
ma moulinette d'adaptation (incomplete).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8685 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4963 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
et Pcompare_antisym
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4962 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4816 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
positifs et naturels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4809 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey
emakarov
gregoire
herbelin