{-# LANGUAGE Trustworthy #-}
module Data.SOP.NP.DeFun (
Append, AppendSym, AppendSym1,
append, appendSym, appendSym1,
Map, MapSym, MapSym1,
map, mapSym, mapSym1,
Concat, ConcatSym,
concat, concatSym,
ConcatMap, ConcatMapSym, ConcatMapSym1,
concatMap, concatMapSym, concatMapSym1,
Map2, Map2Sym, Map2Sym1, Map2Sym2,
map2, map2Sym, map2Sym1, map2Sym2,
Sequence, SequenceSym,
sequence, sequenceSym,
Foldr, FoldrSym, FoldrSym1, FoldrSym2,
foldr, foldrSym, foldrSym1, foldrSym2,
Foldl, FoldlSym, FoldlSym1, FoldlSym2,
foldl, foldlSym, foldlSym1, foldlSym2,
ZipWith, ZipWithSym, ZipWithSym1, ZipWithSym2,
zipWith, zipWithSym, zipWithSym1, zipWithSym2,
Reverse, ReverseSym,
reverse, reverseSym,
) where
import DeFun.List
import Data.SOP.NP (NP (..))
import DeFun.Core
import DeFun.Function
append :: NP a xs -> NP a ys -> NP a (Append xs ys)
append :: forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
Nil NP a ys
ys = NP a ys
ys
append (a x
x :* NP a xs
xs) NP a ys
ys = a x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
xs NP a ys
ys
appendSym :: Lam2 (NP a) (NP a) (NP a) AppendSym
appendSym :: forall {k} (a :: k -> *). Lam2 (NP a) (NP a) (NP a) AppendSym
appendSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xs :: [a]).
NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1
appendSym1 :: NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1 :: forall {a} (a :: a -> *) (xs :: [a]).
NP a xs -> Lam (NP a) (NP a) (AppendSym1 xs)
appendSym1 NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a xs
xs)
map :: Lam a b f -> NP a xs -> NP b (Map f xs)
map :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
(xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
_ NP a xs
Nil = forall {k} (a :: k -> *). NP a '[]
Nil
map Lam a b f
f (a x
x :* NP a xs
xs) = Lam a b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
(xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
f NP a xs
xs
mapSym :: Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym :: forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1
mapSym1 :: Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b).
Lam a b f -> Lam (NP a) (NP b) (MapSym1 f)
mapSym1 Lam a b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> b)
(xs :: [a]).
Lam a b f -> NP a xs -> NP b (Map f xs)
map Lam a b f
f)
concat :: NP (NP a) xss -> NP a (Concat xss)
concat :: forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat NP (NP a) xss
Nil = forall {k} (a :: k -> *). NP a '[]
Nil
concat (NP a x
xs :* NP (NP a) xs
xss) = forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append NP a x
xs (forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat NP (NP a) xs
xss)
concatSym :: Lam (NP (NP a)) (NP a) ConcatSym
concatSym :: forall {k} (a :: k -> *). Lam (NP (NP a)) (NP a) ConcatSym
concatSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP a (Concat xss)
concat
concatMap :: Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
(xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
_ NP a xs
Nil = forall {k} (a :: k -> *). NP a '[]
Nil
concatMap Lam a (NP b) f
f (a x
x :* NP a xs
xs) = forall {a} (a :: a -> *) (xs :: [a]) (ys :: [a]).
NP a xs -> NP a ys -> NP a (Append xs ys)
append (Lam a (NP b) f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x) (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
(xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
f NP a xs
xs)
concatMapSym :: Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
concatMapSym :: forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam2 (a :~> NP b) (NP a) (NP b) ConcatMapSym
concatMapSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b]).
Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1
concatMapSym1 :: Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b]).
Lam a (NP b) f -> Lam (NP a) (NP b) (ConcatMapSym1 f)
concatMapSym1 Lam a (NP b) f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
(xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap Lam a (NP b) f
f)
map2 :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 Lam2 a b c f
f NP a xs
xs NP b ys
ys = forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> [b])
(xs :: [a]).
Lam a (NP b) f -> NP a xs -> NP b (ConcatMap f xs)
concatMap (forall {b1} {c1} {a1} (b2 :: b1 -> *) (c2 :: c1 -> *)
(f :: b1 ~> c1) (a2 :: a1 -> *) (g :: a1 ~> b1).
Lam b2 c2 f -> Lam a2 b2 g -> Lam a2 c2 (CompSym2 f g)
compSym2 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (f :: a1 ~> (b1 ~> c1)) (x :: b1).
Lam2 a2 b2 c2 f -> b2 x -> Lam a2 c2 (FlipSym2 f x)
flipSym2 forall {k} {k} (a :: k -> *) (b :: k -> *).
Lam (a :~> b) (Lam (NP a) (NP b)) MapSym
mapSym NP b ys
ys) Lam2 a b c f
f) NP a xs
xs
map2Sym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) Map2Sym
map2Sym :: forall {k} {k} {k} (a :: k -> *) (b :: k -> *) (c :: k -> *).
Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) Map2Sym
map2Sym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1
map2Sym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (Map2Sym1 f)
map2Sym1 Lam2 a b c f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 Lam2 a b c f
f)
map2Sym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (Map2Sym2 f xs)
map2Sym2 Lam2 a b c f
f NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 Lam2 a b c f
f NP a xs
xs)
sequence :: NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence :: forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence NP (NP a) xss
Nil = forall {k} (a :: k -> *). NP a '[]
Nil forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {k} (a :: k -> *). NP a '[]
Nil
sequence (NP a x
xs :* NP (NP a) xs
xss) = forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (Map2 f xs ys)
map2 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (con :: a1 -> b1 -> c1).
LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con)
con2 forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*)) NP a x
xs (forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence NP (NP a) xs
xss)
sequenceSym :: Lam (NP (NP a)) (NP (NP a)) SequenceSym
sequenceSym :: forall {k} (a :: k -> *). Lam (NP (NP a)) (NP (NP a)) SequenceSym
sequenceSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xss :: [[a]]).
NP (NP a) xss -> NP (NP a) (Sequence xss)
sequence
foldr :: Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
(x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
_ b x
z NP a ys
Nil = b x
z
foldr Lam2 a b b f
f b x
z (a x
x :* NP a xs
xs) = Lam2 a b b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
(x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
f b x
z NP a xs
xs)
foldrSym :: Lam3 (a :~> b :~> b) b (NP a) b FoldrSym
foldrSym :: forall {k} {b} (a :: k -> *) (b :: b -> *).
Lam3 (a :~> (b :~> b)) b (NP a) b FoldrSym
foldrSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b)).
Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1
foldrSym1 :: Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b)).
Lam2 a b b f -> Lam2 b (NP a) b (FoldrSym1 f)
foldrSym1 Lam2 a b b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
(x :: b).
Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 Lam2 a b b f
f)
foldrSym2 :: Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 :: forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
(x :: b).
Lam2 a b b f -> b x -> Lam (NP a) b (FoldrSym2 f x)
foldrSym2 Lam2 a b b f
f b x
z = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} (a :: a -> *) (b :: b -> *) (f :: a ~> (b ~> b))
(x :: b) (ys :: [a]).
Lam2 a b b f -> b x -> NP a ys -> b (Foldr f x ys)
foldr Lam2 a b b f
f b x
z)
foldl :: Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
_ b x
z NP a ys
Nil = b x
z
foldl Lam2 b a b f
f b x
z (a x
x :* NP a xs
xs) = forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
f (Lam2 b a b f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ b x
z forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x) NP a xs
xs
foldlSym :: Lam3 (b :~> a :~> b) b (NP a) b FoldlSym
foldlSym :: forall {b} {k} (b :: b -> *) (a :: k -> *).
Lam3 (b :~> (a :~> b)) b (NP a) b FoldlSym
foldlSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b)).
Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1
foldlSym1 :: Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1 :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b)).
Lam2 b a b f -> Lam2 b (NP a) b (FoldlSym1 f)
foldlSym1 Lam2 b a b f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b).
Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 Lam2 b a b f
f)
foldlSym2 :: Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 :: forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b).
Lam2 b a b f -> b x -> Lam (NP a) b (FoldlSym2 f x)
foldlSym2 Lam2 b a b f
f b x
z = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl Lam2 b a b f
f b x
z)
zipWith :: Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
_ NP a xs
Nil NP b ys
_ = forall {k} (a :: k -> *). NP a '[]
Nil
zipWith Lam2 a b c f
_ (a x
_ :* NP a xs
_) NP b ys
Nil = forall {k} (a :: k -> *). NP a '[]
Nil
zipWith Lam2 a b c f
f (a x
x :* NP a xs
xs) (b x
y :* NP b xs
ys) = Lam2 a b c f
f forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ a x
x forall {a1} {k} (a2 :: a1 -> *) (b :: k -> *) (f :: a1 ~> k)
(x :: a1).
Lam a2 b f -> a2 x -> b (f @@ x)
@@ b x
y forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
:* forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
f NP a xs
xs NP b xs
ys
zipWithSym :: Lam3 (a :~> b :~> c) (NP a) (NP b) (NP c) ZipWithSym
zipWithSym :: forall {k} {k} {k} (a :: k -> *) (b :: k -> *) (c :: k -> *).
Lam3 (a :~> (b :~> c)) (NP a) (NP b) (NP c) ZipWithSym
zipWithSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1
zipWithSym1 :: Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)).
Lam2 a b c f -> Lam2 (NP a) (NP b) (NP c) (ZipWithSym1 f)
zipWithSym1 Lam2 a b c f
f = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 Lam2 a b c f
f)
zipWithSym2 :: Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 :: forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]).
Lam2 a b c f -> NP a xs -> Lam (NP b) (NP c) (ZipWithSym2 f xs)
zipWithSym2 Lam2 a b c f
f NP a xs
xs = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam (forall {a} {b} {c} (a :: a -> *) (b :: b -> *) (c :: c -> *)
(f :: a ~> (b ~> c)) (xs :: [a]) (ys :: [b]).
Lam2 a b c f -> NP a xs -> NP b ys -> NP c (ZipWith f xs ys)
zipWith Lam2 a b c f
f NP a xs
xs)
reverse :: NP a xs -> NP a (Reverse xs)
reverse :: forall {a} (a :: a -> *) (xs :: [a]). NP a xs -> NP a (Reverse xs)
reverse = forall {b} {a} (b :: b -> *) (a :: a -> *) (f :: b ~> (a ~> b))
(x :: b) (ys :: [a]).
Lam2 b a b f -> b x -> NP a ys -> b (Foldl f x ys)
foldl (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (f :: a1 ~> (b1 ~> c1)).
Lam2 a2 b2 c2 f -> Lam2 b2 a2 c2 (FlipSym1 f)
flipSym1 (forall {a1} {b1} {c1} (a2 :: a1 -> *) (b2 :: b1 -> *)
(c2 :: c1 -> *) (con :: a1 -> b1 -> c1).
LamRep2 a2 b2 c2 (Con2 con) -> Lam2 a2 b2 c2 (Con2 con)
con2 forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> NP a xs -> NP a (x : xs)
(:*))) forall {k} (a :: k -> *). NP a '[]
Nil
reverseSym :: Lam (NP a) (NP a) ReverseSym
reverseSym :: forall {k} (a :: k -> *). Lam (NP a) (NP a) ReverseSym
reverseSym = forall a b (a1 :: a -> *) (b1 :: b -> *) (f :: a ~> b).
LamRep a1 b1 f -> Lam a1 b1 f
Lam forall {a} (a :: a -> *) (xs :: [a]). NP a xs -> NP a (Reverse xs)
reverse