Cleanup.

tests/Linear.idr

@@ -9,10 +9,15 @@ toVectFun {n =   Z} _ = Nil
 toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
 
 N : Nat
-N = 320
+N = 800
 
 xs : Vect (S N) Nat
 xs = toVectFun {n = S N} finToNat
 
+fromNat : {n : Nat} -> Nat -> Fin n
+fromNat {n = S m}  Z    = FZ
+fromNat {n = S m} (S i) = if i < m then FS (fromNat i) else last 
+
 main : IO ()
 main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
+-- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))

tests/Linear.lidr

@@ -9,11 +9,15 @@
 > toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
 
 > N : Nat
-> N = 1600
+> N = 800
 
 > xs : Vect (S N) Nat
 > xs = toVectFun {n = S N} finToNat
 
+> fromNat : {n : Nat} -> Nat -> Fin n
+> fromNat {n = S m}  Z    = FZ
+> fromNat {n = S m} (S i) = if i < m then FS (fromNat i) else last 
+
 > main : IO ()
 > main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (toIntegerNat N)) xs))
-
+> -- main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromNat N) xs))