Fix module name for Effect.Default
The file name mismatch with the module name resulted in Effect.Default
not being exported by IdrisDoc. This commit fixes this issue.
commit573fa25401b2c775c2e9fce9f7f8784a4dfac993
authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk>
dateThu 7 Jan 2016, 17:43 (11 years ago)
parent79ff02f
libs/effects/Effect/Default.idr+1−2
@@ -1,4 +1,4 @@
1−module Default
1+module Effect.Default
22
33import Data.Vect
44
@@ -43,4 +43,3 @@ instance Default a => Default (Vect n a) where
4343 mkDef : (n : Nat) -> Vect n a
4444 mkDef Z = []
4545 mkDef (S k) = default :: mkDef k
46−