{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
module Type.Data.Num.Decimal.Digit.Proof (
   Nat(Nat), Pos(Pos),
   UnaryNat(UnaryNat), unaryNat, unaryNatImpl,
   UnaryPos(UnaryPos), unaryPos, unaryPosImpl,
   ) where

import qualified Type.Data.Num.Unary as Unary
import qualified Type.Data.Num.Unary.Proof as UnaryProof
import qualified Type.Data.Num.Decimal.Digit as Digit


data Nat d = (Digit.C d) => Nat
data Pos d = (Digit.Pos d) => Pos

newtype UnaryNatTheorem d =
   UnaryNatTheorem {
      UnaryNatTheorem d -> Nat d -> Nat (ToUnary d)
runUnaryNatTheorem :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)
   }

unaryNatTheorem :: (Unary.Natural (Digit.ToUnary d)) => UnaryNatTheorem d
unaryNatTheorem :: UnaryNatTheorem d
unaryNatTheorem = (Nat d -> Nat (ToUnary d)) -> UnaryNatTheorem d
forall d. (Nat d -> Nat (ToUnary d)) -> UnaryNatTheorem d
UnaryNatTheorem (\Nat d
Nat -> Nat (ToUnary d)
forall x. Natural x => Nat x
UnaryProof.Nat)

unaryNatImpl :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)
unaryNatImpl :: Nat d -> Nat (ToUnary d)
unaryNatImpl d :: Nat d
d@Nat d
Nat =
   UnaryNatTheorem d -> Nat d -> Nat (ToUnary d)
forall d. UnaryNatTheorem d -> Nat d -> Nat (ToUnary d)
runUnaryNatTheorem
      (UnaryNatTheorem Dec0
-> UnaryNatTheorem Dec1
-> UnaryNatTheorem Dec2
-> UnaryNatTheorem Dec3
-> UnaryNatTheorem Dec4
-> UnaryNatTheorem Dec5
-> UnaryNatTheorem Dec6
-> UnaryNatTheorem Dec7
-> UnaryNatTheorem Dec8
-> UnaryNatTheorem Dec9
-> UnaryNatTheorem d
forall d (f :: * -> *).
C d =>
f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f d
Digit.switch
         UnaryNatTheorem Dec0
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec1
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec2
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec3
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem
         UnaryNatTheorem Dec4
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec5
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec6
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec7
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem
         UnaryNatTheorem Dec8
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem UnaryNatTheorem Dec9
forall d. Natural (ToUnary d) => UnaryNatTheorem d
unaryNatTheorem)
      Nat d
d


newtype UnaryPosTheorem d =
   UnaryPosTheorem {
      UnaryPosTheorem d -> Pos d -> Pos (ToUnary d)
runUnaryPosTheorem :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)
   }

unaryPosTheorem :: (Unary.Positive (Digit.ToUnary d)) => UnaryPosTheorem d
unaryPosTheorem :: UnaryPosTheorem d
unaryPosTheorem = (Pos d -> Pos (ToUnary d)) -> UnaryPosTheorem d
forall d. (Pos d -> Pos (ToUnary d)) -> UnaryPosTheorem d
UnaryPosTheorem (\Pos d
Pos -> Pos (ToUnary d)
forall x. Positive x => Pos x
UnaryProof.Pos)

unaryPosImpl :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)
unaryPosImpl :: Pos d -> Pos (ToUnary d)
unaryPosImpl d :: Pos d
d@Pos d
Pos =
   UnaryPosTheorem d -> Pos d -> Pos (ToUnary d)
forall d. UnaryPosTheorem d -> Pos d -> Pos (ToUnary d)
runUnaryPosTheorem
      (UnaryPosTheorem Dec1
-> UnaryPosTheorem Dec2
-> UnaryPosTheorem Dec3
-> UnaryPosTheorem Dec4
-> UnaryPosTheorem Dec5
-> UnaryPosTheorem Dec6
-> UnaryPosTheorem Dec7
-> UnaryPosTheorem Dec8
-> UnaryPosTheorem Dec9
-> UnaryPosTheorem d
forall d (f :: * -> *).
Pos d =>
f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f d
Digit.switchPos
         UnaryPosTheorem Dec1
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec2
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec3
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec4
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem
         UnaryPosTheorem Dec5
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec6
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec7
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem UnaryPosTheorem Dec8
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem
         UnaryPosTheorem Dec9
forall d. Positive (ToUnary d) => UnaryPosTheorem d
unaryPosTheorem)
      Pos d
d



data UnaryNat d = Unary.Natural (Digit.ToUnary d) => UnaryNat

unaryNat :: (Digit.C d) => UnaryNat d
unaryNat :: UnaryNat d
unaryNat =
   UnaryNat Dec0
-> UnaryNat Dec1
-> UnaryNat Dec2
-> UnaryNat Dec3
-> UnaryNat Dec4
-> UnaryNat Dec5
-> UnaryNat Dec6
-> UnaryNat Dec7
-> UnaryNat Dec8
-> UnaryNat Dec9
-> UnaryNat d
forall d (f :: * -> *).
C d =>
f Dec0
-> f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f d
Digit.switch
      UnaryNat Dec0
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec1
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec2
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec3
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec4
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat
      UnaryNat Dec5
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec6
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec7
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec8
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat UnaryNat Dec9
forall d. Natural (ToUnary d) => UnaryNat d
UnaryNat


data UnaryPos d = Unary.Positive (Digit.ToUnary d) => UnaryPos

unaryPos :: (Digit.Pos d) => UnaryPos d
unaryPos :: UnaryPos d
unaryPos =
   UnaryPos Dec1
-> UnaryPos Dec2
-> UnaryPos Dec3
-> UnaryPos Dec4
-> UnaryPos Dec5
-> UnaryPos Dec6
-> UnaryPos Dec7
-> UnaryPos Dec8
-> UnaryPos Dec9
-> UnaryPos d
forall d (f :: * -> *).
Pos d =>
f Dec1
-> f Dec2
-> f Dec3
-> f Dec4
-> f Dec5
-> f Dec6
-> f Dec7
-> f Dec8
-> f Dec9
-> f d
Digit.switchPos
      UnaryPos Dec1
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec2
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec3
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec4
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos
      UnaryPos Dec5
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec6
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec7
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec8
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos UnaryPos Dec9
forall d. Positive (ToUnary d) => UnaryPos d
UnaryPos