git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2886 from jfdm/fix-effect-default
cc95593Jan de Muijnck-Hughes
libs/effects/Effect/Default.idr+1−2
compare with master
unifiedsplit
@@ -1,4 +1,4 @@
1−module Default
1+module Effect.Default
2
2
3import Data.Vect
3import Data.Vect
4
4
@@ -43,4 +43,3 @@ implementation Default a => Default (Vect n a) where
43 mkDef : (n : Nat) -> Vect n a
43 mkDef : (n : Nat) -> Vect n a
44 mkDef Z = []
44 mkDef Z = []
45 mkDef (S k) = default :: mkDef k
45 mkDef (S k) = default :: mkDef k
46−