git.iko.soy/Idris-dev
on ef96397 help sign in
Idris-dev/tutorial/examples/usefultypes.idr
20 lines 474 B history raw
2intVec : Vect Int 5
3intVec = [1, 2, 3, 4, 5]
5double : Int -> Int
6double x = x * 2
8vec : (n ** Vect Int n)
9vec = (_ ** [3, 4])
11list_lookup : Nat -> List a -> Maybe a
12list_lookup _ Nil = Nothing
13list_lookup O (x :: xs) = Just x
14list_lookup (S k) (x :: xs) = list_lookup k xs
16lookup_default : Nat -> List a -> a -> a
17lookup_default i xs def = case list_lookup i xs of
18 Nothing => def
19 Just x => x