{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Fcf.Data.Vinyl (rappend) where

import qualified Data.Vinyl as V
import Fcf

rappend ::
  V.Rec f as ->
  V.Rec f bs ->
  V.Rec f (Eval (as ++ bs))
rappend :: Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs))
rappend Rec f as
V.RNil Rec f bs
ys = Rec f bs
Rec f (Eval (as ++ bs))
ys
rappend (f r
x V.:& Rec f rs
xs) Rec f bs
ys = f r
x f r -> Rec f (rs <> bs) -> Rec f (r : (rs <> bs))
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
V.:& (Rec f rs
xs Rec f rs -> Rec f bs -> Rec f (Eval (rs ++ bs))
forall a (f :: a -> *) (as :: [a]) (bs :: [a]).
Rec f as -> Rec f bs -> Rec f (Eval (as ++ bs))
`rappend` Rec f bs
ys)