git.iko.soy/Idris-dev
on 4e326e4 help sign in
Idris-dev/samples/tutorial/UsefulTypes.idr
21 lines 491 B history raw
1import Data.Vect
3intVec : Vect 5 Int
4intVec = [1, 2, 3, 4, 5]
6double : Int -> Int
7double x = x * 2
9vec : (n ** Vect n Int)
10vec = (_ ** [3, 4])
12list_lookup : Nat -> List a -> Maybe a
13list_lookup _ Nil = Nothing
14list_lookup Z (x :: xs) = Just x
15list_lookup (S k) (x :: xs) = list_lookup k xs
17lookup_default : Nat -> List a -> a -> a
18lookup_default i xs def = case list_lookup i xs of
19 Nothing => def
20 Just x => x