-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Nat and Fin: peano naturals and finite numbers
--   
--   This package provides two simple types, and some tools to work with
--   them. Also on type level as <tt>DataKinds</tt>.
--   
--   <pre>
--   -- Peano naturals
--   data Nat = Z | S Nat
--   
--   -- Finite naturals
--   data Fin (n :: Nat) where
--       Z :: Fin ('S n)
--       S :: Fin n -&gt; Fin ('Nat.S n)
--   </pre>
--   
--   <a>vec</a> implements length-indexed (sized) lists using this package
--   for indexes.
--   
--   The <a>Data.Fin.Enum</a> module let's work generically with
--   enumerations.
--   
--   See <a>Hasochism: the pleasure and pain of dependently typed haskell
--   programming</a> by Sam Lindley and Conor McBride for answers to
--   <i>how</i> and <i>why</i>. Read <a>APLicative Programming with
--   Naperian Functors</a> by Jeremy Gibbons for (not so) different ones.
--   
--   <h3>Similar packages</h3>
--   
--   <ul>
--   <li><a>finite-typelits</a> . Is a great package, but uses
--   <tt>GHC.TypeLits</tt>.</li>
--   <li><a>type-natural</a> depends on <tt>singletons</tt> package.
--   <tt>fin</tt> will try to stay light on the dependencies, and support
--   as many GHC versions as practical.</li>
--   <li><a>peano</a> is very incomplete</li>
--   <li><a>nat</a> as well.</li>
--   <li><a>PeanoWitnesses</a> doesn't use <tt>DataKinds</tt>.</li>
--   <li><a>type-combinators</a> is big package too.</li>
--   </ul>
@package fin
@version 0.1


-- | <a>Nat</a> numbers.
--   
--   This module is designed to be imported qualified.
module Data.Nat

-- | Nat natural numbers.
--   
--   Better than GHC's built-in <a>Nat</a> for some use cases.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Convert <a>Nat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 2
--   2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural $ S $ S $ Z
--   2
--   </pre>
toNatural :: Nat -> Natural

-- | Convert <a>Natural</a> to <a>Nat</a>
--   
--   <pre>
--   &gt;&gt;&gt; fromNatural 4
--   4
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--   </pre>
fromNatural :: Natural -> Nat

-- | Fold <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; cata [] ('x' :) 2
--   "xx"
--   </pre>
cata :: a -> (a -> a) -> Nat -> a

-- | <a>show</a> displaying a structure of <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 0
--   "Z"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 2
--   "S (S Z)"
--   </pre>
explicitShow :: Nat -> String

-- | <a>showsPrec</a> displaying a structure of <a>Nat</a>.
explicitShowsPrec :: Int -> Nat -> ShowS
nat0 :: Nat
nat1 :: Nat
nat2 :: Nat
nat3 :: Nat
nat4 :: Nat
nat5 :: Nat
nat6 :: Nat
nat7 :: Nat
nat8 :: Nat
nat9 :: Nat
instance Data.Data.Data Data.Nat.Nat
instance GHC.Classes.Ord Data.Nat.Nat
instance GHC.Classes.Eq Data.Nat.Nat
instance GHC.Show.Show Data.Nat.Nat
instance GHC.Num.Num Data.Nat.Nat
instance GHC.Real.Real Data.Nat.Nat
instance GHC.Real.Integral Data.Nat.Nat
instance GHC.Enum.Enum Data.Nat.Nat
instance Control.DeepSeq.NFData Data.Nat.Nat
instance Data.Hashable.Class.Hashable Data.Nat.Nat


-- | <a>Nat</a> numbers. <tt>DataKinds</tt> stuff.
--   
--   This module re-exports <a>Data.Nat</a>, and adds type-level things.
module Data.Type.Nat

-- | Nat natural numbers.
--   
--   Better than GHC's built-in <a>Nat</a> for some use cases.
data Nat
Z :: Nat
S :: Nat -> Nat

-- | Convert <a>Nat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 0
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural 2
--   2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toNatural $ S $ S $ Z
--   2
--   </pre>
toNatural :: Nat -> Natural

-- | Convert <a>Natural</a> to <a>Nat</a>
--   
--   <pre>
--   &gt;&gt;&gt; fromNatural 4
--   4
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (fromNatural 4)
--   "S (S (S (S Z)))"
--   </pre>
fromNatural :: Natural -> Nat

-- | Fold <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; cata [] ('x' :) 2
--   "xx"
--   </pre>
cata :: a -> (a -> a) -> Nat -> a

-- | <a>show</a> displaying a structure of <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 0
--   "Z"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow 2
--   "S (S Z)"
--   </pre>
explicitShow :: Nat -> String

-- | <a>showsPrec</a> displaying a structure of <a>Nat</a>.
explicitShowsPrec :: Int -> Nat -> ShowS

-- | Singleton of <a>Nat</a>.
data SNat (n :: Nat)
[SZ] :: SNat  'Z
[SS] :: SNatI n => SNat ( 'S n)

-- | Convert <a>SNat</a> to <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; snatToNat (snat :: SNat Nat1)
--   1
--   </pre>
snatToNat :: forall n. SNat n -> Nat

-- | Convert <a>SNat</a> to <a>Natural</a>
--   
--   <pre>
--   &gt;&gt;&gt; snatToNatural (snat :: SNat Nat0)
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; snatToNatural (snat :: SNat Nat2)
--   2
--   </pre>
snatToNatural :: forall n. SNat n -> Natural

-- | Convenience class to get <a>SNat</a>.
class SNatI (n :: Nat)
snat :: SNatI n => SNat n

-- | Constructor <a>SNatI</a> dictionary from <a>SNat</a>.
withSNat :: SNat n -> (SNatI n => r) -> r

-- | Reify <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; reify nat3 reflect
--   3
--   </pre>
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r

-- | Reflect type-level <a>Nat</a> to the term level.
reflect :: forall n proxy. SNatI n => proxy n -> Nat

-- | As <a>reflect</a> but with any <a>Num</a>.
reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m

-- | Decide equality of type-level numbers.
--   
--   <pre>
--   &gt;&gt;&gt; eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
--   Just Refl
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
--   Nothing
--   </pre>
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)

-- | Type family used to implement <a>==</a> from <a>Data.Type.Equality</a>
--   module.
type family EqNat (n :: Nat) (m :: Nat)

-- | Decide equality of type-level numbers.
--   
--   <pre>
--   &gt;&gt;&gt; decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
--   "Yes Refl"
--   </pre>
discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)

-- | Induction on <a>Nat</a>.
--   
--   Useful in proofs or with GADTs, see source of <a>proofPlusNZero</a>.
induction :: forall n f. SNatI n => f  'Z -> (forall m. SNatI m => f m -> f ( 'S m)) -> f n

-- | Induction on <a>Nat</a>, functor form. Useful for computation.
--   
--   <pre>
--   &gt;&gt;&gt; induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int
--   Tagged 6
--   </pre>
induction1 :: forall n f a. SNatI n => f  'Z a -> (forall m. SNatI m => f m a -> f ( 'S m) a) -> f n a

-- | The induction will be fully inlined.
--   
--   See <tt>test/Inspection.hs</tt>.
class SNatI n => InlineInduction (n :: Nat)
inlineInduction1 :: InlineInduction n => f  'Z a -> (forall m. InlineInduction m => f m a -> f ( 'S m) a) -> f n a

-- | See <a>InlineInduction</a>.
inlineInduction :: forall n f. InlineInduction n => f  'Z -> (forall m. InlineInduction m => f m -> f ( 'S m)) -> f n

-- | Unfold <tt>n</tt> steps of a general recursion.
--   
--   <i>Note:</i> Always <b>benchmark</b>. This function may give you both
--   <i>bad</i> properties: a lot of code (increased binary size), and
--   worse performance.
--   
--   For known <tt>n</tt> <a>unfoldedFix</a> will unfold recursion, for
--   example
--   
--   <pre>
--   <a>unfoldedFix</a> (<a>Proxy</a> :: <a>Proxy</a> <a>Nat3</a>) f = f (f (f (fix f)))
--   </pre>
unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a

-- | Addition.
--   
--   <pre>
--   &gt;&gt;&gt; reflect (snat :: SNat (Plus Nat1 Nat2))
--   3
--   </pre>
type family Plus (n :: Nat) (m :: Nat) :: Nat

-- | Multiplication.
--   
--   <pre>
--   &gt;&gt;&gt; reflect (snat :: SNat (Mult Nat2 Nat3))
--   6
--   </pre>
type family Mult (n :: Nat) (m :: Nat) :: Nat

-- | Convert to GHC <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! ToGHC Nat5
--   ToGHC Nat5 :: GHC.Nat
--   = 5
--   </pre>
type family ToGHC (n :: Nat) :: Nat

-- | Convert from GHC <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; :kind! FromGHC 7
--   FromGHC 7 :: Nat
--   = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
--   </pre>
type family FromGHC (n :: Nat) :: Nat
nat0 :: Nat
nat1 :: Nat
nat2 :: Nat
nat3 :: Nat
nat4 :: Nat
nat5 :: Nat
nat6 :: Nat
nat7 :: Nat
nat8 :: Nat
nat9 :: Nat
type Nat0 =  'Z
type Nat1 =  'S Nat0
type Nat2 =  'S Nat1
type Nat3 =  'S Nat2
type Nat4 =  'S Nat3
type Nat5 =  'S Nat4
type Nat6 =  'S Nat5
type Nat7 =  'S Nat6
type Nat8 =  'S Nat7
type Nat9 =  'S Nat8

-- | <pre>
--   0 + n = n
--   </pre>
proofPlusZeroN :: Plus Nat0 n :~: n

-- | <pre>
--   n + 0 = n
--   </pre>
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n

-- | <pre>
--   0 * n = 0
--   </pre>
proofMultZeroN :: Mult Nat0 n :~: Nat0

-- | <pre>
--   n * 0 = 0
--   </pre>
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0

-- | <pre>
--   1 * n = n
--   </pre>
proofMultOneN :: SNatI n => Mult Nat1 n :~: n

-- | <pre>
--   n * 1 = n
--   </pre>
proofMultNOne :: SNatI n => Mult n Nat1 :~: n
instance GHC.Show.Show a => GHC.Show.Show (Data.Type.Nat.Tagged n a)
instance GHC.Show.Show (Data.Type.Nat.SNat p)
instance Data.Type.Nat.InlineInduction 'Data.Nat.Z
instance Data.Type.Nat.InlineInduction n => Data.Type.Nat.InlineInduction ('Data.Nat.S n)
instance Data.Type.Nat.SNatI 'Data.Nat.Z
instance Data.Type.Nat.SNatI n => Data.Type.Nat.SNatI ('Data.Nat.S n)
instance Data.Type.Equality.TestEquality Data.Nat.Nat Data.Type.Nat.SNat


-- | Finite numbers.
--   
--   This module is designed to be imported as
--   
--   <pre>
--   import Data.Fin (Fin (..))
--   import qualified Data.Fin as Fin
--   </pre>
module Data.Fin

-- | Finite numbers: <tt>[0..n-1]</tt>.
data Fin (n :: Nat)
[FZ] :: Fin ( 'S n)
[FS] :: Fin n -> Fin ( 'S n)

-- | Fold <a>Fin</a>.
cata :: forall a n. a -> (a -> a) -> Fin n -> a

-- | <a>show</a> displaying a structure of <a>Fin</a>.
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (0 :: Fin N.Nat1)
--   "FZ"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; explicitShow (2 :: Fin N.Nat3)
--   "FS (FS FZ)"
--   </pre>
explicitShow :: Fin n -> String

-- | <a>showsPrec</a> displaying a structure of <a>Fin</a>.
explicitShowsPrec :: Int -> Fin n -> ShowS

-- | Convert to <a>Nat</a>.
toNat :: Fin n -> Nat

-- | Convert from <a>Nat</a>.
--   
--   <pre>
--   &gt;&gt;&gt; fromNat N.nat1 :: Maybe (Fin N.Nat2)
--   Just 1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; fromNat N.nat1 :: Maybe (Fin N.Nat1)
--   Nothing
--   </pre>
fromNat :: SNatI n => Nat -> Maybe (Fin n)

-- | Convert to <a>Natural</a>.
toNatural :: Fin n -> Natural

-- | conversion to <a>Integer</a>
toInteger :: Integral a => a -> Integer

-- | Multiplicative inverse.
--   
--   Works for <tt><a>Fin</a> n</tt> where <tt>n</tt> is coprime with an
--   argument, i.e. in general when <tt>n</tt> is prime.
--   
--   <pre>
--   &gt;&gt;&gt; map inverse universe :: [Fin N.Nat5]
--   [0,1,3,2,4]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; zipWith (*) universe (map inverse universe) :: [Fin N.Nat5]
--   [0,1,1,1,1]
--   </pre>
--   
--   Adaptation of <a>pseudo-code in Wikipedia</a>
inverse :: forall n. SNatI n => Fin n -> Fin n

-- | All values. <tt>[minBound .. maxBound]</tt> won't work for
--   <tt><a>Fin</a> <a>Nat0</a></tt>.
--   
--   <pre>
--   &gt;&gt;&gt; universe :: [Fin N.Nat3]
--   [0,1,2]
--   </pre>
universe :: SNatI n => [Fin n]

-- | <a>universe</a> which will be fully inlined, if <tt>n</tt> is known at
--   compile time.
--   
--   <pre>
--   &gt;&gt;&gt; inlineUniverse :: [Fin N.Nat3]
--   [0,1,2]
--   </pre>
inlineUniverse :: InlineInduction n => [Fin n]

-- | Like <a>universe</a> but <a>NonEmpty</a>.
--   
--   <pre>
--   &gt;&gt;&gt; universe1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--   </pre>
universe1 :: SNatI n => NonEmpty (Fin ( 'S n))

-- | <pre>
--   &gt;&gt;&gt; inlineUniverse1 :: NonEmpty (Fin N.Nat3)
--   0 :| [1,2]
--   </pre>
inlineUniverse1 :: InlineInduction n => NonEmpty (Fin ( 'S n))

-- | <tt><a>Fin</a> <a>Nat0</a></tt> is inhabited.
absurd :: Fin Nat0 -> b

-- | Counting to one is boring.
--   
--   <pre>
--   &gt;&gt;&gt; boring
--   0
--   </pre>
boring :: Fin Nat1
weakenLeft :: forall n m. InlineInduction n => Proxy m -> Fin n -> Fin (Plus n m)
weakenRight :: forall n m. InlineInduction n => Proxy n -> Fin m -> Fin (Plus n m)

-- | Append two <a>Fin</a>s together.
--   
--   <pre>
--   &gt;&gt;&gt; append (Left fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
--   2
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; append (Right fin2 :: Either (Fin N.Nat5) (Fin N.Nat4))
--   7
--   </pre>
append :: forall n m. InlineInduction n => Either (Fin n) (Fin m) -> Fin (Plus n m)

-- | Inverse of <a>append</a>.
--   
--   <pre>
--   &gt;&gt;&gt; split fin2 :: Either (Fin N.Nat2) (Fin N.Nat3)
--   Right 0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; split fin1 :: Either (Fin N.Nat2) (Fin N.Nat3)
--   Left 1
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; map split universe :: [Either (Fin N.Nat2) (Fin N.Nat3)]
--   [Left 0,Left 1,Right 0,Right 1,Right 2]
--   </pre>
split :: forall n m. InlineInduction n => Fin (Plus n m) -> Either (Fin n) (Fin m)
fin0 :: Fin (Plus Nat0 ( 'S n))
fin1 :: Fin (Plus Nat1 ( 'S n))
fin2 :: Fin (Plus Nat2 ( 'S n))
fin3 :: Fin (Plus Nat3 ( 'S n))
fin4 :: Fin (Plus Nat4 ( 'S n))
fin5 :: Fin (Plus Nat5 ( 'S n))
fin6 :: Fin (Plus Nat6 ( 'S n))
fin7 :: Fin (Plus Nat7 ( 'S n))
fin8 :: Fin (Plus Nat8 ( 'S n))
fin9 :: Fin (Plus Nat9 ( 'S n))
instance GHC.Classes.Eq (Data.Fin.Fin n)
instance GHC.Classes.Ord (Data.Fin.Fin n)
instance ((n :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m :: Data.Nat.Nat), Data.Type.Nat.SNatI m) => GHC.Enum.Bounded (Data.Fin.Fin n)
instance GHC.Show.Show (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Num.Num (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Real.Real (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Real.Integral (Data.Fin.Fin n)
instance Data.Type.Nat.SNatI n => GHC.Enum.Enum (Data.Fin.Fin n)
instance Control.DeepSeq.NFData (Data.Fin.Fin n)
instance Data.Hashable.Class.Hashable (Data.Fin.Fin n)


-- | This module is designed to be imported qualified:
--   
--   <pre>
--   import qualified Data.Fin.Enum as E
--   </pre>
module Data.Fin.Enum

-- | Generic enumerations.
--   
--   <i>Examples:</i>
--   
--   <pre>
--   &gt;&gt;&gt; from ()
--   0
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; to 0 :: ()
--   ()
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; to 0 :: Bool
--   False
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; map to F.universe :: [Bool]
--   [False,True]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; map (to . (+1) . from) [LT, EQ, GT] :: [Ordering] -- Num Fin is modulo arithmetic
--   [EQ,GT,LT]
--   </pre>
class Enum a where {
    
    -- | The size of an enumeration.
    type family EnumSize a :: Nat;
    type EnumSize a = GEnumSize a;
}

-- | Converts a value to its index.
from :: Enum a => a -> Fin (EnumSize a)

-- | Converts a value to its index.
from :: (Enum a, Generic a, GFrom a, EnumSize a ~ GEnumSize a) => a -> Fin (EnumSize a)

-- | Converts from index to the original value.
to :: Enum a => Fin (EnumSize a) -> a

-- | Converts from index to the original value.
to :: (Enum a, Generic a, GTo a, EnumSize a ~ GEnumSize a) => Fin (EnumSize a) -> a

-- | Generic version of <a>from</a>.
gfrom :: (Generic a, GFrom a) => a -> Fin (GEnumSize a)

-- | Constraint for the class that computes <a>gfrom</a>.
type GFrom a = GFromRep (Rep a)

-- | Generic version of <a>to</a>.
gto :: (Generic a, GTo a) => Fin (GEnumSize a) -> a

-- | Constraint for the class that computes <a>gto</a>.
type GTo a = GToRep (Rep a)

-- | Compute the size from the type.
type GEnumSize a = EnumSizeRep (Rep a) Nat0
instance Data.Fin.Enum.Enum Data.Void.Void
instance Data.Fin.Enum.Enum ()
instance Data.Fin.Enum.Enum GHC.Types.Bool
instance Data.Fin.Enum.Enum GHC.Types.Ordering
instance (Data.Fin.Enum.Enum a, Data.Fin.Enum.Enum b, Data.Type.Nat.InlineInduction (Data.Fin.Enum.EnumSize a)) => Data.Fin.Enum.Enum (Data.Either.Either a b)
instance (Data.Fin.Enum.GToRep a, Data.Fin.Enum.GToRep b) => Data.Fin.Enum.GToRep ((GHC.Generics.:+:) * a b)
instance Data.Fin.Enum.GToRep a => Data.Fin.Enum.GToRep (GHC.Generics.M1 * d c a)
instance Data.Fin.Enum.GToRep (GHC.Generics.V1 *)
instance Data.Fin.Enum.GToRep (GHC.Generics.U1 *)
instance (Data.Fin.Enum.GFromRep a, Data.Fin.Enum.GFromRep b) => Data.Fin.Enum.GFromRep ((GHC.Generics.:+:) * a b)
instance Data.Fin.Enum.GFromRep a => Data.Fin.Enum.GFromRep (GHC.Generics.M1 * d c a)
instance Data.Fin.Enum.GFromRep (GHC.Generics.V1 *)
instance Data.Fin.Enum.GFromRep (GHC.Generics.U1 *)


-- | Less-than-or-equal relation for (unary) natural numbers <a>Nat</a>.
--   
--   There are at least three ways to encode this relation.
--   
--   <ul>
--   <li>&lt;math&gt; and &lt;math&gt; (this module),</li>
--   <li>&lt;math&gt; and &lt;math&gt;
--   (<a>Data.Type.Nat.LE.ReflStep</a>),</li>
--   <li>&lt;math&gt; (tricky in Haskell).</li>
--   </ul>
--   
--   Depending on a situation, usage ergonomics are different.
module Data.Type.Nat.LE

-- | Total order of <a>Nat</a>, less-than-or-Equal-to, &lt;math&gt;.
class LE n m
leProof :: LE n m => LEProof n m

-- | An evidence of &lt;math&gt;. <i>zero+succ</i> definition.
data LEProof n m
[LEZero] :: LEProof  'Z m
[LESucc] :: LEProof n m -> LEProof ( 'S n) ( 'S m)

-- | Constructor <a>LE</a> dictionary from <a>LEProof</a>.
withLEProof :: LEProof n m -> (LE n m => r) -> r

-- | Find the <tt><a>LEProof</a> n m</tt>, i.e. compare numbers.
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)

-- | &lt;math&gt;
leZero :: LEProof  'Z n

-- | &lt;math&gt;
leSucc :: LEProof n m -> LEProof ( 'S n) ( 'S m)

-- | &lt;math&gt;
leRefl :: forall n. SNatI n => LEProof n n

-- | &lt;math&gt;
leStep :: LEProof n m -> LEProof n ( 'S m)

-- | &lt;math&gt;
leAsym :: LEProof n m -> LEProof m n -> n :~: m

-- | &lt;math&gt;
leTrans :: LEProof n m -> LEProof m p -> LEProof n p

-- | &lt;math&gt;
leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ( 'S m) n

-- | &lt;math&gt;
--   
--   <pre>
--   &gt;&gt;&gt; leProof :: LEProof Nat2 Nat3
--   LESucc (LESucc LEZero)
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; leSwap (leSwap' (leProof :: LEProof Nat2 Nat3))
--   LESucc (LESucc (LESucc LEZero))
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; lePred (leSwap (leSwap' (leProof :: LEProof Nat2 Nat3)))
--   LESucc (LESucc LEZero)
--   </pre>
leSwap' :: LEProof n m -> LEProof ( 'S m) n -> void

-- | &lt;math&gt;
leStepL :: LEProof ( 'S n) m -> LEProof n m

-- | &lt;math&gt;
lePred :: LEProof ( 'S n) ( 'S m) -> LEProof n m

-- | &lt;math&gt;
proofZeroLEZero :: LEProof n  'Z -> n :~:  'Z
instance GHC.Show.Show (Data.Type.Nat.LE.LEProof n m)
instance Data.Type.Nat.LE.LE 'Data.Nat.Z m
instance ((m :: Data.Nat.Nat) Data.Type.Equality.~ ('Data.Nat.S m' :: Data.Nat.Nat), Data.Type.Nat.LE.LE n m') => Data.Type.Nat.LE.LE ('Data.Nat.S n) m
instance GHC.Classes.Eq (Data.Type.Nat.LE.LEProof n m)
instance GHC.Classes.Ord (Data.Type.Nat.LE.LEProof n m)
instance (Data.Type.Nat.SNatI n, Data.Type.Nat.SNatI m) => Data.Type.Dec.Decidable (Data.Type.Nat.LE.LEProof n m)

module Data.Type.Nat.LE.ReflStep

-- | An evidence of &lt;math&gt;. <i>refl+step</i> definition.
data LEProof n m
[LERefl] :: LEProof n n
[LEStep] :: LEProof n m -> LEProof n ( 'S m)

-- | Convert from <i>zero+succ</i> to <i>refl+step</i> definition.
--   
--   Inverse of <a>toZeroSucc</a>.
fromZeroSucc :: forall n m. SNatI m => LEProof n m -> LEProof n m

-- | Convert <i>refl+step</i> to <i>zero+succ</i> definition.
--   
--   Inverse of <a>fromZeroSucc</a>.
toZeroSucc :: SNatI n => LEProof n m -> LEProof n m

-- | Find the <tt><a>LEProof</a> n m</tt>, i.e. compare numbers.
decideLE :: forall n m. (SNatI n, SNatI m) => Dec (LEProof n m)

-- | &lt;math&gt;
leZero :: forall n. SNatI n => LEProof  'Z n

-- | &lt;math&gt;
leSucc :: LEProof n m -> LEProof ( 'S n) ( 'S m)

-- | &lt;math&gt;
leRefl :: LEProof n n

-- | &lt;math&gt;
leStep :: LEProof n m -> LEProof n ( 'S m)

-- | &lt;math&gt;
leAsym :: LEProof n m -> LEProof m n -> n :~: m

-- | &lt;math&gt;
leTrans :: LEProof n m -> LEProof m p -> LEProof n p

-- | &lt;math&gt;
leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ( 'S m) n

-- | &lt;math&gt;
leSwap' :: LEProof n m -> LEProof ( 'S m) n -> void

-- | &lt;math&gt;
leStepL :: LEProof ( 'S n) m -> LEProof n m

-- | &lt;math&gt;
lePred :: LEProof ( 'S n) ( 'S m) -> LEProof n m

-- | &lt;math&gt;
proofZeroLEZero :: LEProof n  'Z -> n :~:  'Z
instance GHC.Show.Show (Data.Type.Nat.LE.ReflStep.LEProof n m)
instance GHC.Classes.Eq (Data.Type.Nat.LE.ReflStep.LEProof n m)
instance GHC.Classes.Ord (Data.Type.Nat.LE.ReflStep.LEProof n m)
instance (Data.Type.Nat.SNatI n, Data.Type.Nat.SNatI m) => Data.Type.Dec.Decidable (Data.Type.Nat.LE.ReflStep.LEProof n m)

module Data.Type.Nat.LT

-- | Less-Than-or. &lt;math&gt;. Well-founded relation on <a>Nat</a>.
--   
--   GHC can solve this for us!
--   
--   <pre>
--   &gt;&gt;&gt; ltProof :: LTProof Nat0 Nat4
--   LESucc LEZero
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; ltProof :: LTProof Nat2 Nat4
--   LESucc (LESucc (LESucc LEZero))
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; ltProof :: LTProof Nat3 Nat3
--   ...
--   ...error...
--   ...
--   </pre>
class LT (n :: Nat) (m :: Nat)
ltProof :: LT n m => LTProof n m

-- | An evidence &lt;math&gt; which is the same as (1 + n le m).
type LTProof n m = LEProof ( 'S n) m
withLTProof :: LTProof n m -> (LT n m => r) -> r

-- | &lt;math&gt;
ltReflAbsurd :: LTProof n n -> a

-- | &lt;math&gt;
ltSymAbsurd :: LTProof n m -> LTProof m n -> a

-- | &lt;math&gt;
ltTrans :: LTProof n m -> LTProof m p -> LTProof n p
instance Data.Type.Nat.LE.LE ('Data.Nat.S n) m => Data.Type.Nat.LT.LT n m