git.iko.soy/Idris-dev
on 2d3bbcc help sign in
Idris-dev/samples/tutorial/usefultypes.idr
20 lines 474 B history raw
2intVec : Vect 5 Int
3intVec = [1, 2, 3, 4, 5]
5double : Int -> Int
6double x = x * 2
8vec : (n ** Vect n Int)
9vec = (_ ** [3, 4])
11list_lookup : Nat -> List a -> Maybe a
12list_lookup _ Nil = Nothing
13list_lookup Z (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