diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:18 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:18 +0000 |
commit | a2edf68be812636dc9e6859ea6cda9a1a619fc66 (patch) | |
tree | 0739e72bf0ab046487f958f1b53307d184923f5e /theories/NArith/Ndiv_def.v | |
parent | 865a9a517ce09d1336c2a1e117c25452089a4aa7 (diff) |
NArith: Definition of a Npow power function
By the way, adds an Piter_op iterator :
Piter_op op p a is "a op a ... op a" with a occurring p times.
It could be use to define Pmult_nat and hence nat_of_P (not
fully done for maintaining compatibility).
Unlike iter_pos, Piter_op is logarithmic in p, not linear.
Note: We should adapt someday the brain-damaged Zpower to make it
use Piter_op instead of iter_pos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13543 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/Ndiv_def.v')
0 files changed, 0 insertions, 0 deletions