7ML7W Idris Days 1 2

Chris Patuzzo edited this page Sep 21, 2018 · 2 revisions

TODO

-- A function which takes a value and a list, and returns a
-- list of all elements in the original list greater than the
-- value. We used `Ord` to allow the function to take any type
-- that is "orderable", so characters work as well as numbers
greaterThan : Ord a => a -> List a -> List a
greaterThan v = filter ( > v )

-- Return every other item in the list, starting with the
-- first one
everyOther : List a -> List a
everyOther [] = []
everyOther [x] = [x]
everyOther (x :: y :: rest) = x :: everyOther rest

-- A Vector of a specific size containing members of a specific type
data Vect : Nat -> Type -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

-- Our attempt at defining a function which only adds vectors of
-- the same size
(++) : Vect n a -> Vect n a -> Vect (n + n) a
(++) Nil Nil = Nil
(++) (x :: xs) (y :: ys) = x :: y :: (xs ++ ys)
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.