Nat.golden

Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| plus :: Nat -> Nat -> Nat
          plus Zero m = m
          plus (Succ n) m = Succ (plus n m)
          pred :: Nat -> Nat
          pred Zero = Zero
          pred (Succ n) = n
          
          data Nat
            where
              Zero :: Nat
              Succ :: Nat -> Nat
            deriving (Eq, Show, Read, Ord) |]
  ======>
    data Nat
      where
        Zero :: Nat
        Succ :: Nat -> Nat
      deriving (Eq, Show, Read, Ord)
    plus :: Nat -> Nat -> Nat
    plus Zero m = m
    plus (Succ n) m = Succ (plus n m)
    pred :: Nat -> Nat
    pred Zero = Zero
    pred (Succ n) = n
    type ZeroSym0 :: Nat
    type family ZeroSym0 :: Nat where
      ZeroSym0 = Zero
    type SuccSym0 :: (~>) Nat Nat
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 a0123456789876543210
    type instance Apply @Nat @Nat SuccSym0 a0123456789876543210 = Succ a0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd ((,) SuccSym0KindInference ())
    type SuccSym1 :: Nat -> Nat
    type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where
      SuccSym1 a0123456789876543210 = Succ a0123456789876543210
    type PredSym0 :: (~>) Nat Nat
    data PredSym0 :: (~>) Nat Nat
      where
        PredSym0KindInference :: SameKind (Apply PredSym0 arg) (PredSym1 arg) =>
                                 PredSym0 a0123456789876543210
    type instance Apply @Nat @Nat PredSym0 a0123456789876543210 = Pred a0123456789876543210
    instance SuppressUnusedWarnings PredSym0 where
      suppressUnusedWarnings = snd ((,) PredSym0KindInference ())
    type PredSym1 :: Nat -> Nat
    type family PredSym1 (a0123456789876543210 :: Nat) :: Nat where
      PredSym1 a0123456789876543210 = Pred a0123456789876543210
    type PlusSym0 :: (~>) Nat ((~>) Nat Nat)
    data PlusSym0 :: (~>) Nat ((~>) Nat Nat)
      where
        PlusSym0KindInference :: SameKind (Apply PlusSym0 arg) (PlusSym1 arg) =>
                                 PlusSym0 a0123456789876543210
    type instance Apply @Nat @((~>) Nat Nat) PlusSym0 a0123456789876543210 = PlusSym1 a0123456789876543210
    instance SuppressUnusedWarnings PlusSym0 where
      suppressUnusedWarnings = snd ((,) PlusSym0KindInference ())
    type PlusSym1 :: Nat -> (~>) Nat Nat
    data PlusSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Nat
      where
        PlusSym1KindInference :: SameKind (Apply (PlusSym1 a0123456789876543210) arg) (PlusSym2 a0123456789876543210 arg) =>
                                 PlusSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @Nat @Nat (PlusSym1 a0123456789876543210) a0123456789876543210 = Plus a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (PlusSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) PlusSym1KindInference ())
    type PlusSym2 :: Nat -> Nat -> Nat
    type family PlusSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where
      PlusSym2 a0123456789876543210 a0123456789876543210 = Plus a0123456789876543210 a0123456789876543210
    type Pred :: Nat -> Nat
    type family Pred (a :: Nat) :: Nat where
      Pred Zero = ZeroSym0
      Pred (Succ n) = n
    type Plus :: Nat -> Nat -> Nat
    type family Plus (a :: Nat) (a :: Nat) :: Nat where
      Plus Zero m = m
      Plus (Succ n) m = Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
    type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool
    type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where
      TFHelper_0123456789876543210 Zero Zero = TrueSym0
      TFHelper_0123456789876543210 Zero (Succ _) = FalseSym0
      TFHelper_0123456789876543210 (Succ _) Zero = FalseSym0
      TFHelper_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210
    instance PEq Nat where
      type (==) a a = TFHelper_0123456789876543210 a a
    type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
                                          -> Nat -> GHC.Types.Symbol -> GHC.Types.Symbol
    type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Nat) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
      ShowsPrec_0123456789876543210 _ Zero a_0123456789876543210 = Apply (Apply ShowStringSym0 "Zero") a_0123456789876543210
      ShowsPrec_0123456789876543210 p_0123456789876543210 (Succ arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Succ ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
    instance PShow Nat where
      type ShowsPrec a a a = ShowsPrec_0123456789876543210 a a a
    type Compare_0123456789876543210 :: Nat -> Nat -> Ordering
    type family Compare_0123456789876543210 (a :: Nat) (a :: Nat) :: Ordering where
      Compare_0123456789876543210 Zero Zero = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 (Succ a_0123456789876543210) (Succ b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)
      Compare_0123456789876543210 Zero (Succ _) = LTSym0
      Compare_0123456789876543210 (Succ _) Zero = GTSym0
    instance POrd Nat where
      type Compare a a = Compare_0123456789876543210 a a
    sPred ::
      (forall (t :: Nat). Sing t -> Sing (Pred t :: Nat) :: Type)
    sPlus ::
      (forall (t :: Nat) (t :: Nat).
       Sing t -> Sing t -> Sing (Plus t t :: Nat) :: Type)
    sPred SZero = SZero
    sPred (SSucc (sN :: Sing n)) = sN
    sPlus SZero (sM :: Sing m) = sM
    sPlus (SSucc (sN :: Sing n)) (sM :: Sing m)
      = applySing
          (singFun1 @SuccSym0 SSucc)
          (applySing (applySing (singFun2 @PlusSym0 sPlus) sN) sM)
    instance SingI (PredSym0 :: (~>) Nat Nat) where
      sing = singFun1 @PredSym0 sPred
    instance SingI (PlusSym0 :: (~>) Nat ((~>) Nat Nat)) where
      sing = singFun2 @PlusSym0 sPlus
    instance SingI d =>
             SingI (PlusSym1 (d :: Nat) :: (~>) Nat Nat) where
      sing = singFun1 @(PlusSym1 (d :: Nat)) (sPlus (sing @d))
    instance SingI1 (PlusSym1 :: Nat -> (~>) Nat Nat) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(PlusSym1 (d :: Nat)) (sPlus s)
    data SNat :: Nat -> Type
      where
        SZero :: SNat (Zero :: Nat)
        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
    type instance Sing @Nat = SNat
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ (b :: Demote Nat))
        = (\cases (SomeSing c) -> SomeSing (SSucc c))
            (toSing b :: SomeSing Nat)
    instance SEq Nat => SEq Nat where
      (%==) SZero SZero = STrue
      (%==) SZero (SSucc _) = SFalse
      (%==) (SSucc _) SZero = SFalse
      (%==)
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = applySing
            (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
            sB_0123456789876543210
    instance SShow Nat => SShow Nat where
      sShowsPrec
        _
        SZero
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Zero"))
            sA_0123456789876543210
      sShowsPrec
        (sP_0123456789876543210 :: Sing p_0123456789876543210)
        (SSucc (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (applySing
                  (singFun3 @ShowParenSym0 sShowParen)
                  (applySing
                     (applySing (singFun2 @(>@#@$) (%>)) sP_0123456789876543210)
                     (sFromInteger (sing :: Sing 10))))
               (applySing
                  (applySing
                     (singFun3 @(.@#@$) (%.))
                     (applySing
                        (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Succ ")))
                  (applySing
                     (applySing
                        (singFun3 @ShowsPrecSym0 sShowsPrec)
                        (sFromInteger (sing :: Sing 11)))
                     sArg_0123456789876543210)))
            sA_0123456789876543210
    instance SOrd Nat => SOrd Nat where
      sCompare SZero SZero
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare
        (SSucc (sA_0123456789876543210 :: Sing a_0123456789876543210))
        (SSucc (sB_0123456789876543210 :: Sing b_0123456789876543210))
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            (applySing
               (applySing
                  (singFun2 @(:@#@$) SCons)
                  (applySing
                     (applySing (singFun2 @CompareSym0 sCompare) sA_0123456789876543210)
                     sB_0123456789876543210))
               SNil)
      sCompare SZero (SSucc _) = SLT
      sCompare (SSucc _) SZero = SGT
    instance SDecide Nat => SDecide Nat where
      (%~) SZero SZero = Proved Refl
      (%~) SZero (SSucc _) = Disproved (\case)
      (%~) (SSucc _) SZero = Disproved (\case)
      (%~) (SSucc a) (SSucc b)
        = (\cases
             (Proved Refl) -> Proved Refl
             (Disproved contra) -> Disproved (\cases Refl -> contra Refl))
            ((%~) a b)
    instance Eq (SNat (z :: Nat)) where
      (==) _ _ = True
    instance SDecide Nat =>
             GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat
                                                                   -> Type) where
      GHC.Internal.Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance SDecide Nat =>
             GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat
                                                                   -> Type) where
      GHC.Internal.Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    instance Ord (SNat (z :: Nat)) where
      compare _ _ = EQ
    deriving instance Data.Singletons.ShowSing.ShowSing Nat =>
                      Show (SNat (z :: Nat))
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance SingI1 Succ where
      liftSing = SSucc
    instance SingI (SuccSym0 :: (~>) Nat Nat) where
      sing = singFun1 @SuccSym0 SSucc