Skip to content

Commit

Permalink
dropped explicit indices argument. an interface change, so beware.
Browse files Browse the repository at this point in the history
  • Loading branch information
conal committed Feb 28, 2012
1 parent 37abea3 commit 50f29a1
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 4 deletions.
10 changes: 7 additions & 3 deletions src/TypeUnary/Vec.hs
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion 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
Expand Down

0 comments on commit 50f29a1

Please sign in to comment.