Commit ea549da3 authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent d34db38c
import Data.Fin
import Data.Vect
-- tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
-- toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = 160
N = 320
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
......
......@@ -9,7 +9,7 @@
> toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
> N : Nat
> N = 40
> N = 1600
> xs : Vect (S N) Nat
> xs = toVectFun {n = S N} finToNat
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment