Adding file theories/ZArith/Zsqrt.v that contains a square root function.

actually three functions are provided, one working on positive numbers (it
is structurally recursive), one with a strong specification (Zsqrt), and one with
a weak specification (Zsqrt_plain).  For the function with a weak specification
an extra theorem is also provided.

The decision functions in ZArith_dec have been made transparent so that computation
with the square root function also becomes possible with Lazy Beta Iota Delta Zeta.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions