diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-19 10:16:57 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-19 10:16:57 +0000 |
| commit | b03b65fdc44e3c6cfeceaf997cbc1a50a6c19e5c (patch) | |
| tree | 1f1f559148dc923d883e47bd8941d46ce2446639 /theories/ZArith/vo.itarget | |
| parent | 2521bbc7e9805fd57d2852c1e9631250def11d57 (diff) | |
Add sqrt in Numbers
As for power recently, we add a specification in NZ,N,Z,
derived properties, implementations for nat, N, Z, BigN, BigZ.
- For nat, this sqrt is brand new :-), cf NPeano.v
- For Z, we rework what was in Zsqrt: same algorithm,
no more refine but a pure function, based now on a sqrt
for positive, from which we derive a Nsqrt and a Zsqrt.
For the moment, the old Zsqrt.v file is kept as Zsqrt_compat.v.
It is not loaded by default by Require ZArith.
New definitions are now in Psqrt.v, Zsqrt_def.v and Nsqrt_def.v
- For BigN, BigZ, we changed the specifications to refer to Zsqrt
instead of using characteristic inequations.
On the way, many extensions, in particular BinPos (lemmas about order),
NZMulOrder (results about squares)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13564 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/vo.itarget')
| -rw-r--r-- | theories/ZArith/vo.itarget | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index 59994e32f..28db6848d 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -27,5 +27,6 @@ Zorder.vo Zpow_def.vo Zpower.vo Zpow_facts.vo -Zsqrt.vo +Zsqrt_compat.vo Zwf.vo +Zsqrt_def.vo |