Idris.elm

module Idris exposing (..)


type Num x
    = Z
    | S (Num x)


type Vect ln a
    = Nil
    | Cons a (Vect ln a)


type alias Zero =
    Num ()


empty : Vect Zero x
empty =
    Nil


cons : a -> Vect (Num n) a -> Vect (Num (Num n)) a
cons a vect =
    case vect of
        Nil ->
            Cons a Nil

        Cons x rest ->
            Cons a (cons x rest)


map : (a -> b) -> Vect length a -> Vect length b
map f vect =
    case vect of
        Nil ->
            Nil

        Cons a rest ->
            Cons (f a) (map f rest)