Skip to content

Instantly share code, notes, and snippets.

@bergmark
Created August 5, 2017 19:54
Show Gist options
  • Save bergmark/4f941d1bd24d625a0f3cc31ffd00ed55 to your computer and use it in GitHub Desktop.
Save bergmark/4f941d1bd24d625a0f3cc31ffd00ed55 to your computer and use it in GitHub Desktop.
data Vect : (n: Nat) -> (elem : Type) -> Type where
Empty : Vect 0 elem
OneAnd : elem -> Vect n elem -> Vect (S n) elem
showString : Show elem => Vect n elem -> String
showString Empty = ""
showString (OneAnd x y) = show x ++ showString y
Show elem => Show (Vect n elem) where
show = showString
length : Vect n a -> Nat
length {n} _ = n
empty : Vect Z Int
empty = Empty
one : Vect (S Z) Int
one = OneAnd 1 Empty
append : Vect m a -> Vect n a -> Vect (m + n) a
append Empty Empty = Empty
append Empty v@(OneAnd x y) = v
append v@(OneAnd x z) Empty = OneAnd x (append z Empty)
append v@(OneAnd x z) (OneAnd y w) = OneAnd y (append z (OneAnd y w))
main : IO ()
main = print (append empty empty)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment