singletons-2.5: tests/compile-and-dump/Promote/Prelude.ghc86.template
Promote/Prelude.hs:(0,0)-(0,0): Splicing declarations
promoteOnly
[d| odd :: Nat -> Bool
odd 0 = False
odd n = not . odd $ n - 1 |]
======>
type OddSym1 (a0123456789876543210 :: Nat) =
Odd a0123456789876543210
instance SuppressUnusedWarnings OddSym0 where
suppressUnusedWarnings = snd (((,) OddSym0KindInference) ())
data OddSym0 :: (~>) Nat Bool
where
OddSym0KindInference :: forall a0123456789876543210
arg. SameKind (Apply OddSym0 arg) (OddSym1 arg) =>
OddSym0 a0123456789876543210
type instance Apply OddSym0 a0123456789876543210 = Odd a0123456789876543210
type family Odd (a :: Nat) :: Bool where
Odd 0 = FalseSym0
Odd n = Apply (Apply ($@#@$) (Apply (Apply (.@#@$) NotSym0) OddSym0)) (Apply (Apply (-@#@$) n) (FromInteger 1))