blob: 8cd1004ecff0125da3227dcd6753f404a33c30de (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
module T22623 where
import T22623a
type BindNonEmptyList :: NonEmpty -> NonEmpty -> [Q]
type family BindNonEmptyList (x :: NonEmpty) (y :: NonEmpty) :: [Q] where
BindNonEmptyList ('(:|) a as) c = Tail c ++ Foldr2 a c as
sBindNonEmptyList ::
forall (t :: NonEmpty)
(c :: NonEmpty). SNonEmpty t -> SNonEmpty c -> SList (BindNonEmptyList t c :: [Q])
sBindNonEmptyList
((:%|) (sA :: SQ a) (sAs :: SList as)) (sC :: SNonEmpty c)
= let
sMyHead :: SNonEmpty c -> SQ (MyHead a c)
sMyHead ((:%|) x _) = x
sFoldr :: forall t. SList t -> SList (Foldr2 a c t)
sFoldr SNil = SNil
sFoldr (SCons _ sYs) = SCons (sMyHead sC) (sFoldr sYs)
sF :: Id (SLambda (ConstSym1 c))
sF = SLambda (const sC)
sBs :: SList (Tail c)
_ :%| sBs = applySing sF sA
in
sBs %++ sFoldr sAs
|
