git.iko.soy/Idris-dev
on master help sign in
Remove spurious Data.Fin imports (now reexported by Vect)
44ca9c2BlackBrane
libs/base/Data/HVect.idr−1
compare with master
unifiedsplit
@@ -1,6 +1,5 @@
1module Data.HVect
1module Data.HVect
2
2
3−import Data.Fin
4import public Data.Vect
3import public Data.Vect
5
4
6%access public
5%access public
libs/effects/Effect/Random.idr−1
@@ -2,7 +2,6 @@ module Effect.Random
2
2
3import Effects
3import Effects
4import Data.Vect
4import Data.Vect
5−import Data.Fin
6
5
7data Random : Effect where
6data Random : Effect where
8 getRandom : sig Random Integer Integer
7 getRandom : sig Random Integer Integer