Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data Vect : Nat -> Type -> Type where
- Nil : Vect Z a
- (::) : a -> Vect n a -> Vect (S n) a
- show' : Vect n Int -> String
- show' Nil = "[]"
- show' xs@(_ :: _) = "[" ++ body xs
- where
- body : Vect n Int -> String
- body (x :: xs) = show x ++ ", " ++ body xs
- data Fin : Nat -> Type where
- FZ : Fin Z
- FS : Fin n -> Fin (n + 1)
- take : Fin n -> Vect (n + m) a -> Vect n a
- take = really_believe_me ()
- -- Idris is a strictly evaluated language,
- -- but Idris has so strong pieces of equipment for the halting problem
- main : IO ()
- main = putStrLn . show' $ take (FS (FS FZ)) (1 :: 2 :: Nil)
Add Comment
Please, Sign In to add comment