Merge pull request #2886 from jfdm/fix-effect-default
Fix module name for Effect.Default
commitcc955931eac415035085532bc012428da09b3543
authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com>
dateThu 14 Jan 2016, 10:22 (11 years ago)
parente97f02a573fa25
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 @@ implementation 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−