diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-17 21:00:36 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-17 21:00:36 +0000 |
| commit | f7cf56828fc12726cc1802ea8b2ec1eb709be03c (patch) | |
| tree | db1203b86b37e0b8249dedc061c57aca8a6ce817 /theories/Numbers/Natural | |
| parent | e1cad068ffc188d06c37f46e1bf6e7b57e02e219 (diff) | |
NPeano.modulo : another trick a la "minus" for having a decreasing arg
By writing y instead of 0 in the branch where y is 0,
Coq can see that (modulo x y) is a structural subterm of y
(but not necessarily a strict one).
Same trick for div, but here it doesn't help.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 277223f4b..98809fbf8 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -101,13 +101,13 @@ Fixpoint divmod x y q u := Definition div x y := match y with - | 0 => 0 + | 0 => y | S y' => fst (divmod x y' 0 y') end. Definition modulo x y := match y with - | 0 => 0 + | 0 => y | S y' => y' - snd (divmod x y' 0 y') end. |