diff options
Diffstat (limited to 'src/CHAD/Data.hs')
| -rw-r--r-- | src/CHAD/Data.hs | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/CHAD/Data.hs b/src/CHAD/Data.hs index 8c7605c..63bce5d 100644 --- a/src/CHAD/Data.hs +++ b/src/CHAD/Data.hs @@ -10,6 +10,7 @@ {-# LANGUAGE TypeOperators #-} module CHAD.Data (module CHAD.Data, (:~:)(Refl), If) where +import Data.Bifunctor (first) import Data.Functor.Product import Data.GADT.Compare import Data.GADT.Show @@ -55,6 +56,10 @@ 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) +sunappend :: forall l2 l1 f g. SList f l1 -> SList g (Append l1 l2) -> (SList g l1, SList g l2) +sunappend SNil l = (SNil, l) +sunappend (SCons _ l1) (SCons x l) = first (SCons x) (sunappend l1 l) + type family Replicate n x where Replicate Z x = '[] Replicate (S n) x = x : Replicate n x |