Nat.ghc76.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 instance (:==) Zero Zero = TrueSym0
    type instance (:==) Zero (Succ b) = FalseSym0
    type instance (:==) (Succ a) Zero = FalseSym0
    type instance (:==) (Succ a) (Succ b) = :== a b
    type NatTyCtor = Nat
    type NatTyCtorSym0 = NatTyCtor
    type ZeroSym0 = Zero
    data SuccSym0 (k :: TyFun Nat Nat)
    type instance Apply SuccSym0 a = Succ a
    type family Plus (a :: Nat) (a :: Nat) :: Nat
    type instance Plus Zero m = m
    type instance Plus (Succ n) m =
        Apply SuccSym0 (Apply (Apply PlusSym0 n) m)
    data PlusSym1 (l :: Nat) (l :: TyFun Nat Nat)
    data PlusSym0 (k :: TyFun Nat (TyFun Nat Nat -> *))
    type instance Apply (PlusSym1 a) a = Plus a a
    type instance Apply PlusSym0 a = PlusSym1 a
    type family Pred (a :: Nat) :: Nat
    type instance Pred Zero = ZeroSym0
    type instance Pred (Succ n) = n
    data PredSym0 (k :: TyFun Nat Nat)
    type instance Apply PredSym0 a = Pred a
    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 instance 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