diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:59 +0000 |
| commit | d2bd5d87d23d443f6e41496bdfe5f8e82d675634 (patch) | |
| tree | d9cb49b25b4e49ccda4dd424ef2595f53d9e61c0 /theories/ZArith/Zmisc.v | |
| parent | f1c9bb9d37e3bcefb5838c57e7ae45923d99c4ff (diff) | |
Modularization of BinInt, related fixes in the stdlib
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zmisc.v')
| -rw-r--r-- | theories/ZArith/Zmisc.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index f6b038cbd..6f512e4f3 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -18,16 +18,11 @@ Open Local Scope Z_scope. (** [n]th iteration of the function [f] *) -Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := - match n with - | Z0 => x - | Zpos p => iter_pos p A f x - | Zneg p => x - end. +Notation iter := @Z.iter (only parsing). Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> iter n A f x = iter_nat (Zabs_nat n) A f x. intros n A f x; case n; auto. -intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P. +intros p _; unfold Z.iter, Zabs_nat; apply iter_nat_of_P. intros p abs; case abs; trivial. Qed. |