summaryrefslogtreecommitdiff
path: root/src/Data.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/Data.hs')
-rw-r--r--src/Data.hs9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/Data.hs b/src/Data.hs
index 8c39c6c..eb6c033 100644
--- a/src/Data.hs
+++ b/src/Data.hs
@@ -5,6 +5,7 @@
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Data where
@@ -25,6 +26,14 @@ sappend :: SList f l1 -> SList f l2 -> SList f (Append l1 l2)
sappend SNil l = l
sappend (SCons x xs) l = SCons x (sappend xs l)
+type family Replicate n x where
+ Replicate Z x = '[]
+ Replicate (S n) x = x : Replicate n x
+
+sreplicate :: SNat n -> f t -> SList f (Replicate n t)
+sreplicate SZ _ = SNil
+sreplicate (SS n) x = x `SCons` sreplicate n x
+
data Nat = Z | S Nat
deriving (Show, Eq, Ord)