Guest User

Untitled

a guest
Feb 22nd, 2018
101
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 0.58 KB | None | 0 0
  1. data Vect : Nat -> Type -> Type where
  2. Nil : Vect Z a
  3. (::) : a -> Vect n a -> Vect (S n) a
  4.  
  5. show' : Vect n Int -> String
  6. show' Nil = "[]"
  7. show' xs@(_ :: _) = "[" ++ body xs
  8. where
  9. body : Vect n Int -> String
  10. body (x :: xs) = show x ++ ", " ++ body xs
  11.  
  12. data Fin : Nat -> Type where
  13. FZ : Fin Z
  14. FS : Fin n -> Fin (n + 1)
  15.  
  16. take : Fin n -> Vect (n + m) a -> Vect n a
  17. take = really_believe_me ()
  18.  
  19. -- Idris is a strictly evaluated language,
  20. -- but Idris has so strong pieces of equipment for the halting problem
  21. main : IO ()
  22. main = putStrLn . show' $ take (FS (FS FZ)) (1 :: 2 :: Nil)
Add Comment
Please, Sign In to add comment