Nat.ghc78.template

Singletons/Nat.hs: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) |]
   ======>
     Singletons/Nat.hs:(0,0)-(0,0)
     data Nat
       = Zero | Succ Nat
       deriving (Eq, Show, Read)
     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 family Equals_0123456789 (a :: Nat) (b :: Nat) :: Bool where
       Equals_0123456789 Zero Zero = True
       Equals_0123456789 (Succ a) (Succ b) = (==) a b
       Equals_0123456789 (a :: Nat) (b :: Nat) = False
     type instance (==) (a :: Nat) (b :: Nat) = Equals_0123456789 a b
     type family Plus (a :: Nat) (a :: Nat) :: Nat where
          Plus Zero m = m
          Plus (Succ n) m = Succ (Plus n m)
     type family Pred (a :: Nat) :: Nat where
          Pred Zero = Zero
          Pred (Succ n) = n
     data instance Sing (z :: Nat)
       = z ~ Zero => SZero |
         forall (n :: Nat). z ~ Succ n => SSucc (Sing n)
     type SNat (z :: Nat) = Sing z
     instance SingKind (KProxy :: KProxy Nat) where
       type DemoteRep (KProxy :: KProxy Nat) = Nat
       fromSing SZero = Zero
       fromSing (SSucc b) = Succ (fromSing b)
       toSing Zero = SomeSing SZero
       toSing (Succ b)
         = case toSing b :: SomeSing (KProxy :: KProxy Nat) of {
             SomeSing c -> SomeSing (SSucc c) }
     instance SEq (KProxy :: KProxy Nat) where
       (%:==) SZero SZero = STrue
       (%:==) SZero (SSucc _) = SFalse
       (%:==) (SSucc _) SZero = SFalse
       (%:==) (SSucc a) (SSucc b) = (%:==) a b
     instance SDecide (KProxy :: KProxy Nat) where
       (%~) SZero SZero = Proved Refl
       (%~) SZero (SSucc _)
         = Disproved
             (\case {
                _ -> error "Empty case reached -- this should be impossible" })
       (%~) (SSucc _) SZero
         = Disproved
             (\case {
                _ -> error "Empty case reached -- this should be impossible" })
       (%~) (SSucc a) (SSucc b)
         = case (%~) a b of {
             Proved Refl -> Proved Refl
             Disproved contra -> Disproved (\ Refl -> contra Refl) }
     instance SingI Zero where
       sing = SZero
     instance SingI n => SingI (Succ (n :: Nat)) where
       sing = SSucc sing
     sPlus ::
       forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Plus t t)
     sPlus SZero m = m
     sPlus (SSucc n) m = SSucc (sPlus n m)
     sPred :: forall (t :: Nat). Sing t -> Sing (Pred t)
     sPred SZero = SZero
     sPred (SSucc n) = n