From 50f29a11e33dc94b08dc6c39ca24556fa60130fd Mon Sep 17 00:00:00 2001 From: Conal Elliott Date: Mon, 27 Feb 2012 21:11:12 -0800 Subject: [PATCH] dropped explicit indices argument. an interface change, so beware. --- src/TypeUnary/Vec.hs | 10 +++++++--- type-unary.cabal | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/TypeUnary/Vec.hs b/src/TypeUnary/Vec.hs index 1b85e59..6034fc8 100755 --- a/src/TypeUnary/Vec.hs +++ b/src/TypeUnary/Vec.hs @@ -238,9 +238,13 @@ pokeV' (Succ n) p (a :< as) = do poke p a -- dictionary, remove the sizeOf dependence on @a@. -- | Indices under @n@: 'index0' :< 'index1' :< ... -indices :: Nat n -> Vec n (Index n) -indices Zero = ZVec -indices (Succ n) = index0 :< fmap succI (indices n) +indices :: IsNat n => Vec n (Index n) +indices = indices' nat + +-- Variant of 'indices' with explicit argument. +indices' :: Nat n -> Vec n (Index n) +indices' Zero = ZVec +indices' (Succ n) = index0 :< fmap succI (indices' n) -- TODO: Try reimplementing many Vec functions via foldr. Warning: some -- (most?) will fail because they rely on a polymorphic combining function. diff --git a/type-unary.cabal b/type-unary.cabal index acff5ed..ffab528 100755 --- a/type-unary.cabal +++ b/type-unary.cabal @@ -1,5 +1,5 @@ Name: type-unary -Version: 0.1.18 +Version: 0.2.0 Cabal-Version: >= 1.2 Synopsis: Type-level and typed unary natural numbers, inequality proofs, vectors