module Type.Analyse(Ana,App,Typ,module Type.ANat) where
import Type.ANat
type family Ana t where
Ana (f a0 a1 a2 a3 a4 a5 a6 a7 a8) = App (App (App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 A7 A8 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)) (Ana a7)) (Ana a8)
Ana (f a0 a1 a2 a3 a4 a5 a6 a7) = App (App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 A7 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)) (Ana a7)
Ana (f a0 a1 a2 a3 a4 a5 a6) = App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)
Ana (f a0 a1 a2 a3 a4 a5) = App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)
Ana (f a0 a1 a2 a3 a4) = App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)
Ana (f a0 a1 a2 a3) = App (App (App (App (Typ (f A0 A1 A2 A3 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)
Ana (f a0 a1 a2) = App (App (App (Typ (f A0 A1 A2 )) (Ana a0)) (Ana a1)) (Ana a2)
Ana (f a0 a1) = App (App (Typ (f A0 A1 )) (Ana a0)) (Ana a1)
Ana (f a0) = App (Typ (f A0 )) (Ana a0)
Ana a = Typ a
data App f a
data Typ a