Add integer square root

PrimeSieve.ipkg

@@ -16,6 +16,7 @@ license = "Parity Public License 7.0.0"
 
 -- modules to install
 modules = PrimeSieve
+        , PrimeSieve.Util
 
 -- main file (i.e. file to load at REPL)
 main = PrimeSieve

src/PrimeSieve/Util.idr

@@ -0,0 +1,18 @@
+module PrimeSieve.Util
+
+%default total
+
+||| Integer square root
+export
+isqrt : (Integral t, Ord t) => t -> t
+isqrt n = sqrt' n
+  where
+    sqrt' : t -> t
+    sqrt' a =
+      let b = (a + (n `div` a)) `div` 2
+      in if a > b then sqrt' (assert_smaller a b) else a
+
+||| Nat square root
+export
+sqrtNat : Nat -> Nat
+sqrtNat = integerToNat . isqrt . natToInteger