Skip to content

Instantly share code, notes, and snippets.

@kofigumbs
Created March 30, 2019 17:11
Show Gist options
  • Save kofigumbs/84de9b0a8d85860e17ff0e8fa22fae35 to your computer and use it in GitHub Desktop.
Save kofigumbs/84de9b0a8d85860e17ff0e8fa22fae35 to your computer and use it in GitHub Desktop.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment