#if __GLASGOW_HASKELL__ >= 701
#endif
module Data.Number.Fin.TyDecimal
(
D0, D1, D2, D3, D4, D5, D6, D7, D8, D9, (:.)
, LT_, EQ_, GT_
, Nat, NatNE0
, nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9
, MaxBoundInt8
, MaxBoundInt16
, MaxBoundInt32
, MaxBoundInt64
, MaxBoundWord8
, MaxBoundWord16
, MaxBoundWord32
, MaxBoundWord64
, Succ, succ, pred
, Add, add, minus, subtract
, Compare, compare, NatLE, NatLT, assert_NatLE, min, max
) where
import Prelude hiding (succ, pred, subtract, compare, div, gcd, max, min)
import Data.Typeable (Typeable)
import Data.Proxy (Proxy(Proxy))
import Data.Reflection (Reifies(reflect))
import Data.Number.Fin.TyOrdering
data D0 deriving Typeable
data D1 deriving Typeable
data D2 deriving Typeable
data D3 deriving Typeable
data D4 deriving Typeable
data D5 deriving Typeable
data D6 deriving Typeable
data D7 deriving Typeable
data D8 deriving Typeable
data D9 deriving Typeable
data x :. y deriving Typeable
infixl 5 :.
class Nat_ n => Nat n
instance Nat_ n => Nat n
class NatNE0_ n => NatNE0 n
instance NatNE0_ n => NatNE0 n
class Digit_ d
instance Digit_ D0
instance Digit_ D1
instance Digit_ D2
instance Digit_ D3
instance Digit_ D4
instance Digit_ D5
instance Digit_ D6
instance Digit_ D7
instance Digit_ D8
instance Digit_ D9
class (Reifies n Integer, Nat_ n) => NatNE0_ n
instance NatNE0_ D1
instance NatNE0_ D2
instance NatNE0_ D3
instance NatNE0_ D4
instance NatNE0_ D5
instance NatNE0_ D6
instance NatNE0_ D7
instance NatNE0_ D8
instance NatNE0_ D9
instance NatNE0_ n => NatNE0_ (n:.D0)
instance NatNE0_ n => NatNE0_ (n:.D1)
instance NatNE0_ n => NatNE0_ (n:.D2)
instance NatNE0_ n => NatNE0_ (n:.D3)
instance NatNE0_ n => NatNE0_ (n:.D4)
instance NatNE0_ n => NatNE0_ (n:.D5)
instance NatNE0_ n => NatNE0_ (n:.D6)
instance NatNE0_ n => NatNE0_ (n:.D7)
instance NatNE0_ n => NatNE0_ (n:.D8)
instance NatNE0_ n => NatNE0_ (n:.D9)
class (Reifies n Integer) => Nat_ n
instance Nat_ D0
instance Nat_ D1
instance Nat_ D2
instance Nat_ D3
instance Nat_ D4
instance Nat_ D5
instance Nat_ D6
instance Nat_ D7
instance Nat_ D8
instance Nat_ D9
instance NatNE0_ x => Nat_ (x:.D0)
instance NatNE0_ x => Nat_ (x:.D1)
instance NatNE0_ x => Nat_ (x:.D2)
instance NatNE0_ x => Nat_ (x:.D3)
instance NatNE0_ x => Nat_ (x:.D4)
instance NatNE0_ x => Nat_ (x:.D5)
instance NatNE0_ x => Nat_ (x:.D6)
instance NatNE0_ x => Nat_ (x:.D7)
instance NatNE0_ x => Nat_ (x:.D8)
instance NatNE0_ x => Nat_ (x:.D9)
instance Reifies D0 Integer where reflect _ = 0
instance Reifies D1 Integer where reflect _ = 1
instance Reifies D2 Integer where reflect _ = 2
instance Reifies D3 Integer where reflect _ = 3
instance Reifies D4 Integer where reflect _ = 4
instance Reifies D5 Integer where reflect _ = 5
instance Reifies D6 Integer where reflect _ = 6
instance Reifies D7 Integer where reflect _ = 7
instance Reifies D8 Integer where reflect _ = 8
instance Reifies D9 Integer where reflect _ = 9
instance NatNE0_ x => Reifies (x:.D0) Integer where
reflect p = 10 * reflect (div10 p)
instance NatNE0_ x => Reifies (x:.D1) Integer where
reflect p = 10 * reflect (div10 p) + 1
instance NatNE0_ x => Reifies (x:.D2) Integer where
reflect p = 10 * reflect (div10 p) + 2
instance NatNE0_ x => Reifies (x:.D3) Integer where
reflect p = 10 * reflect (div10 p) + 3
instance NatNE0_ x => Reifies (x:.D4) Integer where
reflect p = 10 * reflect (div10 p) + 4
instance NatNE0_ x => Reifies (x:.D5) Integer where
reflect p = 10 * reflect (div10 p) + 5
instance NatNE0_ x => Reifies (x:.D6) Integer where
reflect p = 10 * reflect (div10 p) + 6
instance NatNE0_ x => Reifies (x:.D7) Integer where
reflect p = 10 * reflect (div10 p) + 7
instance NatNE0_ x => Reifies (x:.D8) Integer where
reflect p = 10 * reflect (div10 p) + 8
instance NatNE0_ x => Reifies (x:.D9) Integer where
reflect p = 10 * reflect (div10 p) + 9
div10 :: proxy (h:.t) -> Proxy h
div10 _ = Proxy
nat0 :: Proxy D0; nat0 = Proxy
nat1 :: Proxy D1; nat1 = Proxy
nat2 :: Proxy D2; nat2 = Proxy
nat3 :: Proxy D3; nat3 = Proxy
nat4 :: Proxy D4; nat4 = Proxy
nat5 :: Proxy D5; nat5 = Proxy
nat6 :: Proxy D6; nat6 = Proxy
nat7 :: Proxy D7; nat7 = Proxy
nat8 :: Proxy D8; nat8 = Proxy
nat9 :: Proxy D9; nat9 = Proxy
type MaxBoundInt8 = D1:.D2:.D7
type MaxBoundInt16 = D3:.D2:.D7:.D6:.D7
type MaxBoundInt32 = D2:.D1:.D4:.D7:.D4:.D8:.D3:.D6:.D4:.D7
type MaxBoundInt64 =
D9:.D2:.D2:.D3:.D3:.D7:.D2:.D0:.D3:.D6:.D8:.D5:.D4:.D7:.D7:.D5:.D8:.D0:.D7
type MaxBoundWord8 = D2:.D5:.D5
type MaxBoundWord16 = D6:.D5:.D5:.D3:.D5
type MaxBoundWord32 = D4:.D2:.D9:.D4:.D9:.D6:.D7:.D2:.D9:.D5
type MaxBoundWord64 =
D1:.D8:.D4:.D4:.D6:.D7:.D4:.D4:.D0:.D7:.D3:.D7:.D0:.D9:.D5:.D5:.D1:.D6:.D1:.D5
class (Nat_ x, NatNE0_ y) => Succ x y | x -> y, y -> x
instance Succ D0 D1
instance Succ D1 D2
instance Succ D2 D3
instance Succ D3 D4
instance Succ D4 D5
instance Succ D5 D6
instance Succ D6 D7
instance Succ D7 D8
instance Succ D8 D9
instance Succ D9 (D1:.D0)
instance (NatNE0_ x) => Succ (x:.D0) (x :.D1)
instance (NatNE0_ x) => Succ (x:.D1) (x :.D2)
instance (NatNE0_ x) => Succ (x:.D2) (x :.D3)
instance (NatNE0_ x) => Succ (x:.D3) (x :.D4)
instance (NatNE0_ x) => Succ (x:.D4) (x :.D5)
instance (NatNE0_ x) => Succ (x:.D5) (x :.D6)
instance (NatNE0_ x) => Succ (x:.D6) (x :.D7)
instance (NatNE0_ x) => Succ (x:.D7) (x :.D8)
instance (NatNE0_ x) => Succ (x:.D8) (x :.D9)
instance (NatNE0_ x, Succ x (y:.d)) => Succ (x:.D9) (y :.d :.D0)
succ :: Succ x y => Proxy x -> Proxy y
succ _ = Proxy
pred :: Succ x y => Proxy y -> Proxy x
pred _ = Proxy
class (Digit_ d, Nat_ x, Nat_ y) => Snoc x d y | x d -> y, y -> x d
instance Snoc D0 D0 D0
instance Snoc D0 D1 D1
instance Snoc D0 D2 D2
instance Snoc D0 D3 D3
instance Snoc D0 D4 D4
instance Snoc D0 D5 D5
instance Snoc D0 D6 D6
instance Snoc D0 D7 D7
instance Snoc D0 D8 D8
instance Snoc D0 D9 D9
instance (Digit_ d, Nat_ (D1:.d)) => Snoc D1 d (D1:.d)
instance (Digit_ d, Nat_ (D2:.d)) => Snoc D2 d (D2:.d)
instance (Digit_ d, Nat_ (D3:.d)) => Snoc D3 d (D3:.d)
instance (Digit_ d, Nat_ (D4:.d)) => Snoc D4 d (D4:.d)
instance (Digit_ d, Nat_ (D5:.d)) => Snoc D5 d (D5:.d)
instance (Digit_ d, Nat_ (D6:.d)) => Snoc D6 d (D6:.d)
instance (Digit_ d, Nat_ (D7:.d)) => Snoc D7 d (D7:.d)
instance (Digit_ d, Nat_ (D8:.d)) => Snoc D8 d (D8:.d)
instance (Digit_ d, Nat_ (D9:.d)) => Snoc D9 d (D9:.d)
instance (Digit_ d', Nat_ (x:.d), Nat_ (x:.d:.d')) => Snoc (x:.d) d' (x:.d:.d')
class (Nat_ x, Nat_ y, Nat_ z) => Add_ x y z | x y -> z, z x -> y
instance (Nat_ y) => Add_ D0 y y
instance (Succ y y1) => Add_ D1 y y1
instance (Succ y y1, Succ y1 y2) => Add_ D2 y y2
instance (Succ y y1, Succ y1 y2, Succ y2 y3) => Add_ D3 y y3
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4
) => Add_ D4 y y4
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4, Succ y4 y5
) => Add_ D5 y y5
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4, Succ y4 y5, Succ y5 y6
) => Add_ D6 y y6
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4, Succ y4 y5, Succ y5 y6
, Succ y6 y7
) => Add_ D7 y y7
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4, Succ y4 y5, Succ y5 y6
, Succ y6 y7, Succ y7 y8
) => Add_ D8 y y8
instance
( Succ y y1, Succ y1 y2, Succ y2 y3
, Succ y3 y4, Succ y4 y5, Succ y5 y6
, Succ y6 y7, Succ y7 y8, Succ y8 y9
) => Add_ D9 y y9
instance (NatNE0_ x, NatNE0_ (z:.dz), Add_ x y' z, Snoc y' dz y)
=> Add_ (x:.D0) y (z:.dz)
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D1 (zh:.dy) z)
=> Add_ (x:.D1) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D2 (zh:.dy) z)
=> Add_ (x:.D2) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D3 (zh:.dy) z)
=> Add_ (x:.D3) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D4 (zh:.dy) z)
=> Add_ (x:.D4) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D5 (zh:.dy) z)
=> Add_ (x:.D5) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D6 (zh:.dy) z)
=> Add_ (x:.D6) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D7 (zh:.dy) z)
=> Add_ (x:.D7) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D8 (zh:.dy) z)
=> Add_ (x:.D8) y z
instance (NatNE0_ x, Nat_ z, Add_ x y' zh, Snoc y' dy y, Add_ D9 (zh:.dy) z)
=> Add_ (x:.D9) y z
class (Add_ x y z, Add_ y x z) => Add x y z | x y -> z, z x -> y, z y -> x
instance (Add_ x y z, Add_ y x z) => Add x y z
add :: Add x y z => Proxy x -> Proxy y -> Proxy z
add _ _ = Proxy
minus :: Add x y z => Proxy z -> Proxy x -> Proxy y
minus _ _ = Proxy
subtract :: Add x y z => Proxy x -> Proxy z -> Proxy y
subtract _ _ = Proxy
class (Nat_ x, Nat_ y) => Compare x y r | x y -> r
instance Compare D0 D0 EQ_
instance Compare D0 D1 LT_
instance Compare D0 D2 LT_
instance Compare D0 D3 LT_
instance Compare D0 D4 LT_
instance Compare D0 D5 LT_
instance Compare D0 D6 LT_
instance Compare D0 D7 LT_
instance Compare D0 D8 LT_
instance Compare D0 D9 LT_
instance NatNE0_ (y:.dy) => Compare D0 (y:.dy) LT_
instance Compare D1 D0 GT_
instance Compare D1 D1 EQ_
instance Compare D1 D2 LT_
instance Compare D1 D3 LT_
instance Compare D1 D4 LT_
instance Compare D1 D5 LT_
instance Compare D1 D6 LT_
instance Compare D1 D7 LT_
instance Compare D1 D8 LT_
instance Compare D1 D9 LT_
instance NatNE0_ (y:.dy) => Compare D1 (y:.dy) LT_
instance Compare D2 D0 GT_
instance Compare D2 D1 GT_
instance Compare D2 D2 EQ_
instance Compare D2 D3 LT_
instance Compare D2 D4 LT_
instance Compare D2 D5 LT_
instance Compare D2 D6 LT_
instance Compare D2 D7 LT_
instance Compare D2 D8 LT_
instance Compare D2 D9 LT_
instance NatNE0_ (y:.dy) => Compare D2 (y:.dy) LT_
instance Compare D3 D0 GT_
instance Compare D3 D1 GT_
instance Compare D3 D2 GT_
instance Compare D3 D3 EQ_
instance Compare D3 D4 LT_
instance Compare D3 D5 LT_
instance Compare D3 D6 LT_
instance Compare D3 D7 LT_
instance Compare D3 D8 LT_
instance Compare D3 D9 LT_
instance NatNE0_ (y:.dy) => Compare D3 (y:.dy) LT_
instance Compare D4 D0 GT_
instance Compare D4 D1 GT_
instance Compare D4 D2 GT_
instance Compare D4 D3 GT_
instance Compare D4 D4 EQ_
instance Compare D4 D5 LT_
instance Compare D4 D6 LT_
instance Compare D4 D7 LT_
instance Compare D4 D8 LT_
instance Compare D4 D9 LT_
instance NatNE0_ (y:.dy) => Compare D4 (y:.dy) LT_
instance Compare D5 D0 GT_
instance Compare D5 D1 GT_
instance Compare D5 D2 GT_
instance Compare D5 D3 GT_
instance Compare D5 D4 GT_
instance Compare D5 D5 EQ_
instance Compare D5 D6 LT_
instance Compare D5 D7 LT_
instance Compare D5 D8 LT_
instance Compare D5 D9 LT_
instance NatNE0_ (y:.dy) => Compare D5 (y:.dy) LT_
instance Compare D6 D0 GT_
instance Compare D6 D1 GT_
instance Compare D6 D2 GT_
instance Compare D6 D3 GT_
instance Compare D6 D4 GT_
instance Compare D6 D5 GT_
instance Compare D6 D6 EQ_
instance Compare D6 D7 LT_
instance Compare D6 D8 LT_
instance Compare D6 D9 LT_
instance NatNE0_ (y:.dy) => Compare D6 (y:.dy) LT_
instance Compare D7 D0 GT_
instance Compare D7 D1 GT_
instance Compare D7 D2 GT_
instance Compare D7 D3 GT_
instance Compare D7 D4 GT_
instance Compare D7 D5 GT_
instance Compare D7 D6 GT_
instance Compare D7 D7 EQ_
instance Compare D7 D8 LT_
instance Compare D7 D9 LT_
instance NatNE0_ (y:.dy) => Compare D7 (y:.dy) LT_
instance Compare D8 D0 GT_
instance Compare D8 D1 GT_
instance Compare D8 D2 GT_
instance Compare D8 D3 GT_
instance Compare D8 D4 GT_
instance Compare D8 D5 GT_
instance Compare D8 D6 GT_
instance Compare D8 D7 GT_
instance Compare D8 D8 EQ_
instance Compare D8 D9 LT_
instance NatNE0_ (y:.dy) => Compare D8 (y:.dy) LT_
instance Compare D9 D0 GT_
instance Compare D9 D1 GT_
instance Compare D9 D2 GT_
instance Compare D9 D3 GT_
instance Compare D9 D4 GT_
instance Compare D9 D5 GT_
instance Compare D9 D6 GT_
instance Compare D9 D7 GT_
instance Compare D9 D8 GT_
instance Compare D9 D9 EQ_
instance NatNE0_ (y:.dy) => Compare D9 (y:.dy) LT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D0 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D1 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D2 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D3 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D4 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D5 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D6 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D7 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D8 GT_
instance NatNE0_ (x:.dx) => Compare (x:.dx) D9 GT_
instance
( NatNE0_ (x:.dx), NatNE0_ (y:.dy)
, Compare dx dy dr, Compare x y r', NCS r' dr r
) => Compare (x:.dx) (y:.dy) r
compare :: Compare x y r => Proxy x -> Proxy y -> Proxy r
compare _ _ = Proxy
class (Nat_ x, Nat_ y) => NatLE x y
instance NatLE D0 D0
instance NatLE D0 D1
instance NatLE D0 D2
instance NatLE D0 D3
instance NatLE D0 D4
instance NatLE D0 D5
instance NatLE D0 D6
instance NatLE D0 D7
instance NatLE D0 D8
instance NatLE D0 D9
instance NatNE0_ (y:.dy) => NatLE D0 (y:.dy)
instance NatLE D1 D1
instance NatLE D1 D2
instance NatLE D1 D3
instance NatLE D1 D4
instance NatLE D1 D5
instance NatLE D1 D6
instance NatLE D1 D7
instance NatLE D1 D8
instance NatLE D1 D9
instance NatNE0_ (y:.dy) => NatLE D1 (y:.dy)
instance NatLE D2 D2
instance NatLE D2 D3
instance NatLE D2 D4
instance NatLE D2 D5
instance NatLE D2 D6
instance NatLE D2 D7
instance NatLE D2 D8
instance NatLE D2 D9
instance NatNE0_ (y:.dy) => NatLE D2 (y:.dy)
instance NatLE D3 D3
instance NatLE D3 D4
instance NatLE D3 D5
instance NatLE D3 D6
instance NatLE D3 D7
instance NatLE D3 D8
instance NatLE D3 D9
instance NatNE0_ (y:.dy) => NatLE D3 (y:.dy)
instance NatLE D4 D4
instance NatLE D4 D5
instance NatLE D4 D6
instance NatLE D4 D7
instance NatLE D4 D8
instance NatLE D4 D9
instance NatNE0_ (y:.dy) => NatLE D4 (y:.dy)
instance NatLE D5 D5
instance NatLE D5 D6
instance NatLE D5 D7
instance NatLE D5 D8
instance NatLE D5 D9
instance NatNE0_ (y:.dy) => NatLE D5 (y:.dy)
instance NatLE D6 D6
instance NatLE D6 D7
instance NatLE D6 D8
instance NatLE D6 D9
instance NatNE0_ (y:.dy) => NatLE D6 (y:.dy)
instance NatLE D7 D7
instance NatLE D7 D8
instance NatLE D7 D9
instance NatNE0_ (y:.dy) => NatLE D7 (y:.dy)
instance NatLE D8 D8
instance NatLE D8 D9
instance NatNE0_ (y:.dy) => NatLE D8 (y:.dy)
instance NatLE D9 D9
instance NatNE0_ (y:.dy) => NatLE D9 (y:.dy)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D0) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D1) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D1) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D2) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D2) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D3) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D3) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D4) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D4) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D5) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D5) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D6) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D6) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D7) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D7) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D8) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D8) (y:.D9)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D0)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D1)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D2)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D3)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D4)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D5)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D6)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D7)
instance (NatNE0_ x, NatNE0_ y, Compare x y LT_) => NatLE (x:.D9) (y:.D8)
instance (NatNE0_ x, NatNE0_ y, NatLE x y) => NatLE (x:.D9) (y:.D9)
assert_NatLE :: NatLE x y => Proxy x -> Proxy y -> ()
assert_NatLE Proxy Proxy = ()
class (Nat_ x, NatNE0_ y) => NatLT x y
instance (Succ y' y, NatLE x y') => NatLT x y
class Max_ x y r z | x y r -> z
instance Max_ x y LT_ y
instance Max_ x y EQ_ y
instance Max_ x y GT_ x
max :: (Compare x y r, Max_ x y r z) => Proxy x -> Proxy y -> Proxy z
max _ _ = Proxy
class Min_ x y r z | x y r -> z
instance Min_ x y LT_ x
instance Min_ x y EQ_ x
instance Min_ x y GT_ y
min :: (Compare x y r, Min_ x y r z) => Proxy x -> Proxy y -> Proxy z
min _ _ = Proxy