git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/effects/Effect/Default.idr
46 lines 810 B history raw
1module Default
3import Data.Vect
5class Default a where
6 default : a
8instance Default Int where
9 default = 0
11instance Default Integer where
12 default = 0
14instance Default Float where
15 default = 0
17instance Default Nat where
18 default = 0
20instance Default Char where
21 default = '\0'
23instance Default String where
24 default = ""
26instance Default Bool where
27 default = False
29instance Default () where
30 default = ()
32instance (Default a, Default b) => Default (a, b) where
33 default = (default, default)
35instance Default (Maybe a) where
36 default = Nothing
38instance Default (List a) where
39 default = []
41instance Default a => Default (Vect n a) where
42 default = mkDef _ where
43 mkDef : (n : Nat) -> Vect n a
44 mkDef Z = []
45 mkDef (S k) = default :: mkDef k