Remove spurious Data.Fin imports (now reexported by Vect)
commit44ca9c2d6a6f1eef5ba5319472ce75567a4821f2
authorBlackBrane <cs.hbar@gmail.com>
dateSun 2 Aug 2015, 19:49 (11 years ago)
parent5a08c2c
libs/base/Data/HVect.idr−1
@@ -1,6 +1,5 @@
11module Data.HVect
22
3−import Data.Fin
43import public Data.Vect
54
65%access public
libs/effects/Effect/Random.idr−1
@@ -2,7 +2,6 @@ module Effect.Random
22
33import Effects
44import Data.Vect
5−import Data.Fin
65
76data Random : Effect where
87 getRandom : sig Random Integer Integer