diff options
Diffstat (limited to 'src/Data.hs')
-rw-r--r-- | src/Data.hs | 9 |
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) |