Commit 6f823db8 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 040b2810
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 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 {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = 160
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
main : IO ()
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
> import Data.Fin
> import Data.Vect
> tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
> tail f = f . FS
> toVectFun : {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 = 40
> xs : Vect (S N) Nat
> xs = toVectFun {n = S N} finToNat
> main : IO ()
> main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (toIntegerNat N)) xs))
myS : Nat -> Nat
myS n = S n
myS_crash : Nat -> Nat
myS_crash = S
main : IO ()
main = do
printLn (S Z)
printLn (myS Z)
printLn (myS_crash Z)
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