cosmesis

src/Data/Vec.hs

@@ -17,11 +17,11 @@
 -- new dependantly typed language features in haskell
 module Data.Vec where
 
-import Relation.Equality (gcastWith, cong, sym)
+import Relation.Equality (gcastWith)
 import Data.Nat
 import Data.Bool
 import Data.Char         (Char)
-import Data.Function     ((∘), ($))
+import Data.Function     ((∘))
 import Data.TypeClass    (Show, Eq, Ord, Num, IsList, IsString)
 import Data.Singletons   (SingI, sing)
 
@@ -31,7 +31,7 @@ import qualified Data.TypeClass as T
 infixr 5 :-
 
 -- | The 'Vec' datatype
-data Vec (a ∷ ★) ∷ ℕ → ★ where
+data Vec ∷ ★ → ℕ → ★ where
   Nil  ∷ Vec a Z                   -- ^ empty 'Vec', length 0
   (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator
 
@@ -171,7 +171,7 @@ intercalate xs xss = concat (intersperse xs xss)
 -- | The 'transpose' function transposes the rows and columns of its argument.
 -- For example,
 --
--- > transpose [[1,2,3],[4,5,6]] == [[1,4],[2,5],[3,6]]
+-- > transpose [[1,2,3],[4,5,6]] ≡ [[1,4],[2,5],[3,6]]
 --
 transpose ∷ SingI n ⇒ Vec (Vec a n) m → Vec (Vec a m) n
 transpose Nil         = replicate Nil
@@ -311,7 +311,7 @@ drop' (SS n) (x :- xs) = drop' n xs
 --
 -- 'zip' is right-lazy:
 --
--- > zip Nil ⊥ = Nil
+-- > zip Nil ⊥ ≡ Nil
 zip ∷ Vec a n → Vec b m → Vec (a, b) (Min n m)
 zip = zipWith (,)
 
@@ -323,7 +323,7 @@ zip = zipWith (,)
 --
 -- 'zipWith' is right-lazy:
 --
--- > zipWith f Nil ⊥ = Nil
+-- > zipWith f Nil ⊥ ≡ Nil
 zipWith ∷ (a → b → c) → Vec a n → Vec b m → Vec c (Min n m)
 zipWith _ Nil _ = Nil
 zipWith _ _ Nil = Nil