Data.Type.Natural
data Nat
data SSym0 l
type SSym1 t
type ZSym0
type SNat
data family Sing a
type family Min arg0 arg1 :: a0
type family Max arg0 arg1 :: a0
data MinSym0 l0
data MinSym1 l0 l1
type MinSym2 t0 t1
data MaxSym0 l0
data MaxSym1 l0 l1
type MaxSym2 t0 t1
type n :+: m
type family arg0 :+ arg1 :: a0
data (:+$) l0
data l0 :+$$ l1
type t0 :+$$$ t1
type family arg0 :* arg1 :: a0
type n :*: m
data (:*$) l0
data l0 :*$$ l1
type t0 :*$$$ t1
type n :-: m
type family arg0 :- arg1 :: a0
type n :**: m
data (:-$) l0
data l0 :-$$ l1
type t0 :-$$$ t1
data Leq n m
class n :<= m
data (:<<=$) l
data l :<<=$$ l
type t :<<=$$$ t
type LeqInstance n m
type LeqTrueInstance a b
Leqtype ZeroSym0
type OneSym0
type TwoSym0
type ThreeSym0
type FourSym0
type FiveSym0
type SixSym0
type SevenSym0
type EightSym0
type NineSym0
type TenSym0
type ElevenSym0
type TwelveSym0
type ThirteenSym0
type FourteenSym0
type FifteenSym0
type SixteenSym0
type SeventeenSym0
type EighteenSym0
type NineteenSym0
type TwentySym0
type N0Sym0
type N1Sym0
type N2Sym0
type N3Sym0
type N4Sym0
type N5Sym0
type N6Sym0
type N7Sym0
type N8Sym0
type N9Sym0
type N10Sym0
type N11Sym0
type N12Sym0
type N13Sym0
type N14Sym0
type N15Sym0
type N16Sym0
type N17Sym0
type N18Sym0
type N19Sym0
type N20Sym0