singletons-2.1: tests/compile-and-dump/Singletons/LetStatements.ghc80.template
Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations
singletons
[d| foo1 :: Nat -> Nat
foo1 x
= let
y :: Nat
y = Succ Zero
in y
foo2 :: Nat
foo2
= let
y = Succ Zero
z = Succ y
in z
foo3 :: Nat -> Nat
foo3 x
= let
y :: Nat
y = Succ x
in y
foo4 :: Nat -> Nat
foo4 x
= let
f :: Nat -> Nat
f y = Succ y
in f x
foo5 :: Nat -> Nat
foo5 x
= let
f :: Nat -> Nat
f y
= let
z :: Nat
z = Succ y
in Succ z
in f x
foo6 :: Nat -> Nat
foo6 x
= let
f :: Nat -> Nat
f y = Succ y in
let
z :: Nat
z = f x
in z
foo7 :: Nat -> Nat
foo7 x
= let
x :: Nat
x = Zero
in x
foo8 :: Nat -> Nat
foo8 x
= let
z :: Nat
z = (\ x -> x) Zero
in z
foo9 :: Nat -> Nat
foo9 x
= let
z :: Nat -> Nat
z = (\ x -> x)
in z x
foo10 :: Nat -> Nat
foo10 x
= let
(+) :: Nat -> Nat -> Nat
Zero + m = m
(Succ n) + m = Succ (n + m)
in (Succ Zero) + x
foo11 :: Nat -> Nat
foo11 x
= let
(+) :: Nat -> Nat -> Nat
Zero + m = m
(Succ n) + m = Succ (n + m)
z :: Nat
z = x
in (Succ Zero) + z
foo12 :: Nat -> Nat
foo12 x
= let
(+) :: Nat -> Nat -> Nat
Zero + m = m
(Succ n) + m = Succ (n + x)
in x + (Succ (Succ Zero))
foo13 :: forall a. a -> a
foo13 x
= let
bar :: a
bar = x
in foo13_ bar
foo13_ :: a -> a
foo13_ y = y
foo14 :: Nat -> (Nat, Nat)
foo14 x = let (y, z) = (Succ x, x) in (z, y) |]
======>
foo1 :: Nat -> Nat
foo1 x
= let
y :: Nat
y = Succ Zero
in y
foo2 :: Nat
foo2
= let
y = Succ Zero
z = Succ y
in z
foo3 :: Nat -> Nat
foo3 x
= let
y :: Nat
y = Succ x
in y
foo4 :: Nat -> Nat
foo4 x
= let
f :: Nat -> Nat
f y = Succ y
in f x
foo5 :: Nat -> Nat
foo5 x
= let
f :: Nat -> Nat
f y
= let
z :: Nat
z = Succ y
in Succ z
in f x
foo6 :: Nat -> Nat
foo6 x
= let
f :: Nat -> Nat
f y = Succ y in
let
z :: Nat
z = f x
in z
foo7 :: Nat -> Nat
foo7 x
= let
x :: Nat
x = Zero
in x
foo8 :: Nat -> Nat
foo8 x
= let
z :: Nat
z = (\ x -> x) Zero
in z
foo9 :: Nat -> Nat
foo9 x
= let
z :: Nat -> Nat
z = \ x -> x
in z x
foo10 :: Nat -> Nat
foo10 x
= let
(+) :: Nat -> Nat -> Nat
(+) Zero m = m
(+) (Succ n) m = Succ (n + m)
in ((Succ Zero) + x)
foo11 :: Nat -> Nat
foo11 x
= let
(+) :: Nat -> Nat -> Nat
z :: Nat
(+) Zero m = m
(+) (Succ n) m = Succ (n + m)
z = x
in ((Succ Zero) + z)
foo12 :: Nat -> Nat
foo12 x
= let
(+) :: Nat -> Nat -> Nat
(+) Zero m = m
(+) (Succ n) m = Succ (n + x)
in (x + (Succ (Succ Zero)))
foo13 :: forall a. a -> a
foo13 x
= let
bar :: a
bar = x
in foo13_ bar
foo13_ :: forall a. a -> a
foo13_ y = y
foo14 :: Nat -> (Nat, Nat)
foo14 x = let (y, z) = (Succ x, x) in (z, y)
type family Case_0123456789 x t where
Case_0123456789 x '(y_0123456789, _z_0123456789) = y_0123456789
type family Case_0123456789 x t where
Case_0123456789 x '(_z_0123456789, y_0123456789) = y_0123456789
type Let0123456789YSym1 t = Let0123456789Y t
instance SuppressUnusedWarnings Let0123456789YSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
data Let0123456789YSym0 l
= forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
Let0123456789YSym0KindInference
type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
type Let0123456789ZSym1 t = Let0123456789Z t
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type Let0123456789X_0123456789Sym1 t = Let0123456789X_0123456789 t
instance SuppressUnusedWarnings Let0123456789X_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,)
Let0123456789X_0123456789Sym0KindInference GHC.Tuple.())
data Let0123456789X_0123456789Sym0 l
= forall arg. KindOf (Apply Let0123456789X_0123456789Sym0 arg) ~ KindOf (Let0123456789X_0123456789Sym1 arg) =>
Let0123456789X_0123456789Sym0KindInference
type instance Apply Let0123456789X_0123456789Sym0 l = Let0123456789X_0123456789Sym1 l
type family Let0123456789Y x where
Let0123456789Y x = Case_0123456789 x (Let0123456789X_0123456789Sym1 x)
type family Let0123456789Z x where
Let0123456789Z x = Case_0123456789 x (Let0123456789X_0123456789Sym1 x)
type family Let0123456789X_0123456789 x where
Let0123456789X_0123456789 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x
type Let0123456789BarSym1 t = Let0123456789Bar t
instance SuppressUnusedWarnings Let0123456789BarSym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Let0123456789BarSym0KindInference GHC.Tuple.())
data Let0123456789BarSym0 l
= forall arg. KindOf (Apply Let0123456789BarSym0 arg) ~ KindOf (Let0123456789BarSym1 arg) =>
Let0123456789BarSym0KindInference
type instance Apply Let0123456789BarSym0 l = Let0123456789BarSym1 l
type family Let0123456789Bar x :: a where
Let0123456789Bar x = x
type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
(:<<<%%%%%%%%%%:+) t t t
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
(:<<<%%%%%%%%%%:+$$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$) l
(l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
(:<<<%%%%%%%%%%:+$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$) l
= forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
(:<<<%%%%%%%%%%:+$###)
type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
(:<<<%%%%%%%%%%:+) x Zero m = m
(:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) x)
type Let0123456789ZSym1 t = Let0123456789Z t
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
(:<<<%%%%%%%%%%:+) t t t
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
(:<<<%%%%%%%%%%:+$$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$) l
(l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
(:<<<%%%%%%%%%%:+$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$) l
= forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
(:<<<%%%%%%%%%%:+$###)
type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
type family Let0123456789Z x :: Nat where
Let0123456789Z x = x
type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
(:<<<%%%%%%%%%%:+) x Zero m = m
(:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) m)
type (:<<<%%%%%%%%%%:+$$$$) t (t :: Nat) (t :: Nat) =
(:<<<%%%%%%%%%%:+) t t t
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$$) l (l :: Nat) (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$$) l l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$$) l l arg) =>
(:<<<%%%%%%%%%%:+$$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$$) l l) l = (:<<<%%%%%%%%%%:+$$$$) l l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$$) l
(l :: TyFun Nat (TyFun Nat Nat -> GHC.Types.Type))
= forall arg. KindOf (Apply ((:<<<%%%%%%%%%%:+$$) l) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$$) l arg) =>
(:<<<%%%%%%%%%%:+$$###)
type instance Apply ((:<<<%%%%%%%%%%:+$$) l) l = (:<<<%%%%%%%%%%:+$$$) l l
instance SuppressUnusedWarnings (:<<<%%%%%%%%%%:+$) where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) (:<<<%%%%%%%%%%:+$###) GHC.Tuple.())
data (:<<<%%%%%%%%%%:+$) l
= forall arg. KindOf (Apply (:<<<%%%%%%%%%%:+$) arg) ~ KindOf ((:<<<%%%%%%%%%%:+$$) arg) =>
(:<<<%%%%%%%%%%:+$###)
type instance Apply (:<<<%%%%%%%%%%:+$) l = (:<<<%%%%%%%%%%:+$$) l
type family (:<<<%%%%%%%%%%:+) x (a :: Nat) (a :: Nat) :: Nat where
(:<<<%%%%%%%%%%:+) x Zero m = m
(:<<<%%%%%%%%%%:+) x (Succ n) m = Apply SuccSym0 (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) n) m)
type family Lambda_0123456789 x a_0123456789 t where
Lambda_0123456789 x a_0123456789 x = x
type Lambda_0123456789Sym3 t t t = Lambda_0123456789 t t t
instance SuppressUnusedWarnings Lambda_0123456789Sym2 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym2KindInference GHC.Tuple.())
data Lambda_0123456789Sym2 l l l
= forall arg. KindOf (Apply (Lambda_0123456789Sym2 l l) arg) ~ KindOf (Lambda_0123456789Sym3 l l arg) =>
Lambda_0123456789Sym2KindInference
type instance Apply (Lambda_0123456789Sym2 l l) l = Lambda_0123456789Sym3 l l l
instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
data Lambda_0123456789Sym1 l l
= forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
Lambda_0123456789Sym1KindInference
type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
data Lambda_0123456789Sym0 l
= forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
Lambda_0123456789Sym0KindInference
type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
type Let0123456789ZSym2 t (t :: Nat) = Let0123456789Z t t
instance SuppressUnusedWarnings Let0123456789ZSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym1KindInference GHC.Tuple.())
data Let0123456789ZSym1 l (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply (Let0123456789ZSym1 l) arg) ~ KindOf (Let0123456789ZSym2 l arg) =>
Let0123456789ZSym1KindInference
type instance Apply (Let0123456789ZSym1 l) l = Let0123456789ZSym2 l l
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type family Let0123456789Z x (a :: Nat) :: Nat where
Let0123456789Z x a_0123456789 = Apply (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789) a_0123456789
type family Lambda_0123456789 x t where
Lambda_0123456789 x x = x
type Lambda_0123456789Sym2 t t = Lambda_0123456789 t t
instance SuppressUnusedWarnings Lambda_0123456789Sym1 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym1KindInference GHC.Tuple.())
data Lambda_0123456789Sym1 l l
= forall arg. KindOf (Apply (Lambda_0123456789Sym1 l) arg) ~ KindOf (Lambda_0123456789Sym2 l arg) =>
Lambda_0123456789Sym1KindInference
type instance Apply (Lambda_0123456789Sym1 l) l = Lambda_0123456789Sym2 l l
instance SuppressUnusedWarnings Lambda_0123456789Sym0 where
suppressUnusedWarnings _
= snd
(GHC.Tuple.(,) Lambda_0123456789Sym0KindInference GHC.Tuple.())
data Lambda_0123456789Sym0 l
= forall arg. KindOf (Apply Lambda_0123456789Sym0 arg) ~ KindOf (Lambda_0123456789Sym1 arg) =>
Lambda_0123456789Sym0KindInference
type instance Apply Lambda_0123456789Sym0 l = Lambda_0123456789Sym1 l
type Let0123456789ZSym1 t = Let0123456789Z t
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type family Let0123456789Z x :: Nat where
Let0123456789Z x = Apply (Apply Lambda_0123456789Sym0 x) ZeroSym0
type Let0123456789XSym1 t = Let0123456789X t
instance SuppressUnusedWarnings Let0123456789XSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789XSym0KindInference GHC.Tuple.())
data Let0123456789XSym0 l
= forall arg. KindOf (Apply Let0123456789XSym0 arg) ~ KindOf (Let0123456789XSym1 arg) =>
Let0123456789XSym0KindInference
type instance Apply Let0123456789XSym0 l = Let0123456789XSym1 l
type family Let0123456789X x :: Nat where
Let0123456789X x = ZeroSym0
type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
instance SuppressUnusedWarnings Let0123456789FSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
data Let0123456789FSym1 l (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
Let0123456789FSym1KindInference
type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
instance SuppressUnusedWarnings Let0123456789FSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
data Let0123456789FSym0 l
= forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
Let0123456789FSym0KindInference
type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
type family Let0123456789F x (a :: Nat) :: Nat where
Let0123456789F x y = Apply SuccSym0 y
type Let0123456789ZSym1 t = Let0123456789Z t
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type family Let0123456789Z x :: Nat where
Let0123456789Z x = Apply (Let0123456789FSym1 x) x
type Let0123456789ZSym2 t t = Let0123456789Z t t
instance SuppressUnusedWarnings Let0123456789ZSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym1KindInference GHC.Tuple.())
data Let0123456789ZSym1 l l
= forall arg. KindOf (Apply (Let0123456789ZSym1 l) arg) ~ KindOf (Let0123456789ZSym2 l arg) =>
Let0123456789ZSym1KindInference
type instance Apply (Let0123456789ZSym1 l) l = Let0123456789ZSym2 l l
instance SuppressUnusedWarnings Let0123456789ZSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789ZSym0KindInference GHC.Tuple.())
data Let0123456789ZSym0 l
= forall arg. KindOf (Apply Let0123456789ZSym0 arg) ~ KindOf (Let0123456789ZSym1 arg) =>
Let0123456789ZSym0KindInference
type instance Apply Let0123456789ZSym0 l = Let0123456789ZSym1 l
type family Let0123456789Z x y :: Nat where
Let0123456789Z x y = Apply SuccSym0 y
type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
instance SuppressUnusedWarnings Let0123456789FSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
data Let0123456789FSym1 l (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
Let0123456789FSym1KindInference
type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
instance SuppressUnusedWarnings Let0123456789FSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
data Let0123456789FSym0 l
= forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
Let0123456789FSym0KindInference
type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
type family Let0123456789F x (a :: Nat) :: Nat where
Let0123456789F x y = Apply SuccSym0 (Let0123456789ZSym2 x y)
type Let0123456789FSym2 t (t :: Nat) = Let0123456789F t t
instance SuppressUnusedWarnings Let0123456789FSym1 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym1KindInference GHC.Tuple.())
data Let0123456789FSym1 l (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply (Let0123456789FSym1 l) arg) ~ KindOf (Let0123456789FSym2 l arg) =>
Let0123456789FSym1KindInference
type instance Apply (Let0123456789FSym1 l) l = Let0123456789FSym2 l l
instance SuppressUnusedWarnings Let0123456789FSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789FSym0KindInference GHC.Tuple.())
data Let0123456789FSym0 l
= forall arg. KindOf (Apply Let0123456789FSym0 arg) ~ KindOf (Let0123456789FSym1 arg) =>
Let0123456789FSym0KindInference
type instance Apply Let0123456789FSym0 l = Let0123456789FSym1 l
type family Let0123456789F x (a :: Nat) :: Nat where
Let0123456789F x y = Apply SuccSym0 y
type Let0123456789YSym1 t = Let0123456789Y t
instance SuppressUnusedWarnings Let0123456789YSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
data Let0123456789YSym0 l
= forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
Let0123456789YSym0KindInference
type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
type family Let0123456789Y x :: Nat where
Let0123456789Y x = Apply SuccSym0 x
type Let0123456789YSym0 = Let0123456789Y
type Let0123456789ZSym0 = Let0123456789Z
type family Let0123456789Y where
Let0123456789Y = Apply SuccSym0 ZeroSym0
type family Let0123456789Z where
Let0123456789Z = Apply SuccSym0 Let0123456789YSym0
type Let0123456789YSym1 t = Let0123456789Y t
instance SuppressUnusedWarnings Let0123456789YSym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Let0123456789YSym0KindInference GHC.Tuple.())
data Let0123456789YSym0 l
= forall arg. KindOf (Apply Let0123456789YSym0 arg) ~ KindOf (Let0123456789YSym1 arg) =>
Let0123456789YSym0KindInference
type instance Apply Let0123456789YSym0 l = Let0123456789YSym1 l
type family Let0123456789Y x :: Nat where
Let0123456789Y x = Apply SuccSym0 ZeroSym0
type Foo14Sym1 (t :: Nat) = Foo14 t
instance SuppressUnusedWarnings Foo14Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo14Sym0KindInference GHC.Tuple.())
data Foo14Sym0 (l :: TyFun Nat (Nat, Nat))
= forall arg. KindOf (Apply Foo14Sym0 arg) ~ KindOf (Foo14Sym1 arg) =>
Foo14Sym0KindInference
type instance Apply Foo14Sym0 l = Foo14Sym1 l
type Foo13_Sym1 (t :: a0123456789) = Foo13_ t
instance SuppressUnusedWarnings Foo13_Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo13_Sym0KindInference GHC.Tuple.())
data Foo13_Sym0 (l :: TyFun a0123456789 a0123456789)
= forall arg. KindOf (Apply Foo13_Sym0 arg) ~ KindOf (Foo13_Sym1 arg) =>
Foo13_Sym0KindInference
type instance Apply Foo13_Sym0 l = Foo13_Sym1 l
type Foo13Sym1 (t :: a0123456789) = Foo13 t
instance SuppressUnusedWarnings Foo13Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo13Sym0KindInference GHC.Tuple.())
data Foo13Sym0 (l :: TyFun a0123456789 a0123456789)
= forall arg. KindOf (Apply Foo13Sym0 arg) ~ KindOf (Foo13Sym1 arg) =>
Foo13Sym0KindInference
type instance Apply Foo13Sym0 l = Foo13Sym1 l
type Foo12Sym1 (t :: Nat) = Foo12 t
instance SuppressUnusedWarnings Foo12Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo12Sym0KindInference GHC.Tuple.())
data Foo12Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo12Sym0 arg) ~ KindOf (Foo12Sym1 arg) =>
Foo12Sym0KindInference
type instance Apply Foo12Sym0 l = Foo12Sym1 l
type Foo11Sym1 (t :: Nat) = Foo11 t
instance SuppressUnusedWarnings Foo11Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo11Sym0KindInference GHC.Tuple.())
data Foo11Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo11Sym0 arg) ~ KindOf (Foo11Sym1 arg) =>
Foo11Sym0KindInference
type instance Apply Foo11Sym0 l = Foo11Sym1 l
type Foo10Sym1 (t :: Nat) = Foo10 t
instance SuppressUnusedWarnings Foo10Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo10Sym0KindInference GHC.Tuple.())
data Foo10Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo10Sym0 arg) ~ KindOf (Foo10Sym1 arg) =>
Foo10Sym0KindInference
type instance Apply Foo10Sym0 l = Foo10Sym1 l
type Foo9Sym1 (t :: Nat) = Foo9 t
instance SuppressUnusedWarnings Foo9Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo9Sym0KindInference GHC.Tuple.())
data Foo9Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo9Sym0 arg) ~ KindOf (Foo9Sym1 arg) =>
Foo9Sym0KindInference
type instance Apply Foo9Sym0 l = Foo9Sym1 l
type Foo8Sym1 (t :: Nat) = Foo8 t
instance SuppressUnusedWarnings Foo8Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo8Sym0KindInference GHC.Tuple.())
data Foo8Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo8Sym0 arg) ~ KindOf (Foo8Sym1 arg) =>
Foo8Sym0KindInference
type instance Apply Foo8Sym0 l = Foo8Sym1 l
type Foo7Sym1 (t :: Nat) = Foo7 t
instance SuppressUnusedWarnings Foo7Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo7Sym0KindInference GHC.Tuple.())
data Foo7Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo7Sym0 arg) ~ KindOf (Foo7Sym1 arg) =>
Foo7Sym0KindInference
type instance Apply Foo7Sym0 l = Foo7Sym1 l
type Foo6Sym1 (t :: Nat) = Foo6 t
instance SuppressUnusedWarnings Foo6Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo6Sym0KindInference GHC.Tuple.())
data Foo6Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo6Sym0 arg) ~ KindOf (Foo6Sym1 arg) =>
Foo6Sym0KindInference
type instance Apply Foo6Sym0 l = Foo6Sym1 l
type Foo5Sym1 (t :: Nat) = Foo5 t
instance SuppressUnusedWarnings Foo5Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo5Sym0KindInference GHC.Tuple.())
data Foo5Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo5Sym0 arg) ~ KindOf (Foo5Sym1 arg) =>
Foo5Sym0KindInference
type instance Apply Foo5Sym0 l = Foo5Sym1 l
type Foo4Sym1 (t :: Nat) = Foo4 t
instance SuppressUnusedWarnings Foo4Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo4Sym0KindInference GHC.Tuple.())
data Foo4Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo4Sym0 arg) ~ KindOf (Foo4Sym1 arg) =>
Foo4Sym0KindInference
type instance Apply Foo4Sym0 l = Foo4Sym1 l
type Foo3Sym1 (t :: Nat) = Foo3 t
instance SuppressUnusedWarnings Foo3Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo3Sym0KindInference GHC.Tuple.())
data Foo3Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo3Sym0 arg) ~ KindOf (Foo3Sym1 arg) =>
Foo3Sym0KindInference
type instance Apply Foo3Sym0 l = Foo3Sym1 l
type Foo2Sym0 = Foo2
type Foo1Sym1 (t :: Nat) = Foo1 t
instance SuppressUnusedWarnings Foo1Sym0 where
suppressUnusedWarnings _
= snd (GHC.Tuple.(,) Foo1Sym0KindInference GHC.Tuple.())
data Foo1Sym0 (l :: TyFun Nat Nat)
= forall arg. KindOf (Apply Foo1Sym0 arg) ~ KindOf (Foo1Sym1 arg) =>
Foo1Sym0KindInference
type instance Apply Foo1Sym0 l = Foo1Sym1 l
type family Foo14 (a :: Nat) :: (Nat, Nat) where
Foo14 x = Apply (Apply Tuple2Sym0 (Let0123456789ZSym1 x)) (Let0123456789YSym1 x)
type family Foo13_ (a :: a) :: a where
Foo13_ y = y
type family Foo13 (a :: a) :: a where
Foo13 x = Apply Foo13_Sym0 (Let0123456789BarSym1 x)
type family Foo12 (a :: Nat) :: Nat where
Foo12 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0))
type family Foo11 (a :: Nat) :: Nat where
Foo11 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 ZeroSym0)) (Let0123456789ZSym1 x)
type family Foo10 (a :: Nat) :: Nat where
Foo10 x = Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) (Apply SuccSym0 ZeroSym0)) x
type family Foo9 (a :: Nat) :: Nat where
Foo9 x = Apply (Let0123456789ZSym1 x) x
type family Foo8 (a :: Nat) :: Nat where
Foo8 x = Let0123456789ZSym1 x
type family Foo7 (a :: Nat) :: Nat where
Foo7 x = Let0123456789XSym1 x
type family Foo6 (a :: Nat) :: Nat where
Foo6 x = Let0123456789ZSym1 x
type family Foo5 (a :: Nat) :: Nat where
Foo5 x = Apply (Let0123456789FSym1 x) x
type family Foo4 (a :: Nat) :: Nat where
Foo4 x = Apply (Let0123456789FSym1 x) x
type family Foo3 (a :: Nat) :: Nat where
Foo3 x = Let0123456789YSym1 x
type family Foo2 :: Nat where
Foo2 = Let0123456789ZSym0
type family Foo1 (a :: Nat) :: Nat where
Foo1 x = Let0123456789YSym1 x
sFoo14 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo14Sym0 t :: (Nat, Nat))
sFoo13_ ::
forall (t :: a). Sing t -> Sing (Apply Foo13_Sym0 t :: a)
sFoo13 :: forall (t :: a). Sing t -> Sing (Apply Foo13Sym0 t :: a)
sFoo12 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo12Sym0 t :: Nat)
sFoo11 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo11Sym0 t :: Nat)
sFoo10 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo10Sym0 t :: Nat)
sFoo9 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo9Sym0 t :: Nat)
sFoo8 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo8Sym0 t :: Nat)
sFoo7 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo7Sym0 t :: Nat)
sFoo6 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo6Sym0 t :: Nat)
sFoo5 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo5Sym0 t :: Nat)
sFoo4 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo4Sym0 t :: Nat)
sFoo3 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo3Sym0 t :: Nat)
sFoo2 :: Sing (Foo2Sym0 :: Nat)
sFoo1 ::
forall (t :: Nat). Sing t -> Sing (Apply Foo1Sym0 t :: Nat)
sFoo14 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo14Sym0 t :: (Nat, Nat))
lambda x
= let
sY :: Sing (Let0123456789YSym1 x)
sZ :: Sing (Let0123456789ZSym1 x)
sX_0123456789 :: Sing (Let0123456789X_0123456789Sym1 x)
sY
= case sX_0123456789 of {
STuple2 sY_0123456789 _s_z_0123456789
-> let
lambda ::
forall y_0123456789 _z_0123456789.
Apply (Apply Tuple2Sym0 y_0123456789) _z_0123456789 ~ Let0123456789X_0123456789Sym1 x =>
Sing y_0123456789
-> Sing _z_0123456789
-> Sing (Case_0123456789 x (Apply (Apply Tuple2Sym0 y_0123456789) _z_0123456789))
lambda y_0123456789 _z_0123456789 = y_0123456789
in lambda sY_0123456789 _s_z_0123456789 } ::
Sing (Case_0123456789 x (Let0123456789X_0123456789Sym1 x))
sZ
= case sX_0123456789 of {
STuple2 _s_z_0123456789 sY_0123456789
-> let
lambda ::
forall _z_0123456789 y_0123456789.
Apply (Apply Tuple2Sym0 _z_0123456789) y_0123456789 ~ Let0123456789X_0123456789Sym1 x =>
Sing _z_0123456789
-> Sing y_0123456789
-> Sing (Case_0123456789 x (Apply (Apply Tuple2Sym0 _z_0123456789) y_0123456789))
lambda _z_0123456789 y_0123456789 = y_0123456789
in lambda _s_z_0123456789 sY_0123456789 } ::
Sing (Case_0123456789 x (Let0123456789X_0123456789Sym1 x))
sX_0123456789
= applySing
(applySing
(singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2)
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) x))
x
in
applySing
(applySing (singFun2 (Proxy :: Proxy Tuple2Sym0) STuple2) sZ) sY
in lambda sX
sFoo13_ sY
= let
lambda ::
forall y. t ~ y => Sing y -> Sing (Apply Foo13_Sym0 t :: a)
lambda y = y
in lambda sY
sFoo13 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo13Sym0 t :: a)
lambda x
= let
sBar :: Sing (Let0123456789BarSym1 x :: a)
sBar = x
in applySing (singFun1 (Proxy :: Proxy Foo13_Sym0) sFoo13_) sBar
in lambda sX
sFoo12 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo12Sym0 t :: Nat)
lambda x
= let
(%:+) ::
forall (t :: Nat) (t :: Nat).
Sing t
-> Sing t
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
(%:+) SZero sM
= let
lambda ::
forall m.
(t ~ ZeroSym0, t ~ m) =>
Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda m = m
in lambda sM
(%:+) (SSucc sN) sM
= let
lambda ::
forall n m.
(t ~ Apply SuccSym0 n, t ~ m) =>
Sing n
-> Sing m
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda n m
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
x)
in lambda sN sM
in
applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) x)
(applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
in lambda sX
sFoo11 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo11Sym0 t :: Nat)
lambda x
= let
sZ :: Sing (Let0123456789ZSym1 x :: Nat)
(%:+) ::
forall (t :: Nat) (t :: Nat).
Sing t
-> Sing t
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
sZ = x
(%:+) SZero sM
= let
lambda ::
forall m.
(t ~ ZeroSym0, t ~ m) =>
Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda m = m
in lambda sM
(%:+) (SSucc sN) sM
= let
lambda ::
forall n m.
(t ~ Apply SuccSym0 n, t ~ m) =>
Sing n
-> Sing m
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda n m
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
m)
in lambda sN sM
in
applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+))
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
sZ
in lambda sX
sFoo10 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo10Sym0 t :: Nat)
lambda x
= let
(%:+) ::
forall (t :: Nat) (t :: Nat).
Sing t
-> Sing t
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
(%:+) SZero sM
= let
lambda ::
forall m.
(t ~ ZeroSym0, t ~ m) =>
Sing m -> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda m = m
in lambda sM
(%:+) (SSucc sN) sM
= let
lambda ::
forall n m.
(t ~ Apply SuccSym0 n, t ~ m) =>
Sing n
-> Sing m
-> Sing (Apply (Apply ((:<<<%%%%%%%%%%:+$$) x) t) t :: Nat)
lambda n m
= applySing
(singFun1 (Proxy :: Proxy SuccSym0) SSucc)
(applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+)) n)
m)
in lambda sN sM
in
applySing
(applySing
(singFun2 (Proxy :: Proxy ((:<<<%%%%%%%%%%:+$$) x)) (%:+))
(applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero))
x
in lambda sX
sFoo9 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo9Sym0 t :: Nat)
lambda x
= let
sZ ::
forall (t :: Nat).
Sing t -> Sing (Apply (Let0123456789ZSym1 x) t :: Nat)
sZ sA_0123456789
= let
lambda ::
forall a_0123456789.
t ~ a_0123456789 =>
Sing a_0123456789 -> Sing (Apply (Let0123456789ZSym1 x) t :: Nat)
lambda a_0123456789
= applySing
(singFun1
(Proxy ::
Proxy (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789))
(\ sX
-> let
lambda ::
forall x.
Sing x
-> Sing (Apply (Apply (Apply Lambda_0123456789Sym0 x) a_0123456789) x)
lambda x = x
in lambda sX))
a_0123456789
in lambda sA_0123456789
in
applySing (singFun1 (Proxy :: Proxy (Let0123456789ZSym1 x)) sZ) x
in lambda sX
sFoo8 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo8Sym0 t :: Nat)
lambda x
= let
sZ :: Sing (Let0123456789ZSym1 x :: Nat)
sZ
= applySing
(singFun1
(Proxy :: Proxy (Apply Lambda_0123456789Sym0 x))
(\ sX
-> let
lambda ::
forall x.
Sing x -> Sing (Apply (Apply Lambda_0123456789Sym0 x) x)
lambda x = x
in lambda sX))
SZero
in sZ
in lambda sX
sFoo7 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo7Sym0 t :: Nat)
lambda x
= let
sX :: Sing (Let0123456789XSym1 x :: Nat)
sX = SZero
in sX
in lambda sX
sFoo6 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo6Sym0 t :: Nat)
lambda x
= let
sF ::
forall (t :: Nat).
Sing t -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
sF sY
= let
lambda ::
forall y.
t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
lambda y = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
in lambda sY in
let
sZ :: Sing (Let0123456789ZSym1 x :: Nat)
sZ
= applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
in sZ
in lambda sX
sFoo5 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo5Sym0 t :: Nat)
lambda x
= let
sF ::
forall (t :: Nat).
Sing t -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
sF sY
= let
lambda ::
forall y.
t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
lambda y
= let
sZ :: Sing (Let0123456789ZSym2 x y :: Nat)
sZ = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
in applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) sZ
in lambda sY
in
applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
in lambda sX
sFoo4 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo4Sym0 t :: Nat)
lambda x
= let
sF ::
forall (t :: Nat).
Sing t -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
sF sY
= let
lambda ::
forall y.
t ~ y => Sing y -> Sing (Apply (Let0123456789FSym1 x) t :: Nat)
lambda y = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) y
in lambda sY
in
applySing (singFun1 (Proxy :: Proxy (Let0123456789FSym1 x)) sF) x
in lambda sX
sFoo3 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo3Sym0 t :: Nat)
lambda x
= let
sY :: Sing (Let0123456789YSym1 x :: Nat)
sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) x
in sY
in lambda sX
sFoo2
= let
sY :: Sing Let0123456789YSym0
sZ :: Sing Let0123456789ZSym0
sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero
sZ = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) sY
in sZ
sFoo1 sX
= let
lambda ::
forall x. t ~ x => Sing x -> Sing (Apply Foo1Sym0 t :: Nat)
lambda x
= let
sY :: Sing (Let0123456789YSym1 x :: Nat)
sY = applySing (singFun1 (Proxy :: Proxy SuccSym0) SSucc) SZero
in sY
in lambda sX