diff options
| author | letouzey | 2010-12-17 21:00:36 +0000 |
|---|---|---|
| committer | letouzey | 2010-12-17 21:00:36 +0000 |
| commit | f7cf56828fc12726cc1802ea8b2ec1eb709be03c (patch) | |
| tree | db1203b86b37e0b8249dedc061c57aca8a6ce817 /dev/base_include | |
| 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 'dev/base_include')
0 files changed, 0 insertions, 0 deletions