Data.Type.Natural

Type level peano natural number, some arithmetic functions and their singletons.

Re-exported modules.

module Data.Singletons

Natural Numbers

Peano natural numbers. It will be promoted to the type-level natural number.

data Nat

Constructors

Z

S Nat

Instances

Enum Nat

Defined in Data.Type.Natural.Definitions

Methods

succ :: Nat -> Nat

pred :: Nat -> Nat

toEnum :: Int -> Nat

fromEnum :: Nat -> Int

enumFrom :: Nat -> [Nat]

enumFromThen :: Nat -> Nat -> [Nat]

enumFromTo :: Nat -> Nat -> [Nat]

enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]

Eq Nat

Defined in Data.Type.Natural.Definitions

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Num Nat

Defined in Data.Type.Natural.Definitions

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

Defined in Data.Type.Natural.Definitions

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat

Defined in Data.Type.Natural.Definitions

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

SingKind Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type Demote Nat = (r :: *)

Methods

fromSing :: Sing a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

PEnum Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type Succ arg :: a

type Pred arg :: a

type ToEnum arg :: a

type FromEnum arg :: Nat

type EnumFromTo arg arg1 :: [a]

type EnumFromThenTo arg arg1 arg2 :: [a]

SEnum Nat

Defined in Data.Type.Natural.Definitions

Methods

sSucc :: Sing t -> Sing (Apply SuccSym0 t)

sPred :: Sing t -> Sing (Apply PredSym0 t)

sToEnum :: Sing t -> Sing (Apply ToEnumSym0 t)

sFromEnum :: Sing t -> Sing (Apply FromEnumSym0 t)

sEnumFromTo :: Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2)

sEnumFromThenTo :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3)

PShow Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Nat => SShow Nat

Defined in Data.Type.Natural.Definitions

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

PNum Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type arg + arg1 :: a

type arg - arg1 :: a

type arg * arg1 :: a

type Negate arg :: a

type Abs arg :: a

type Signum arg :: a

type FromInteger arg :: a

SNum Nat

Defined in Data.Type.Natural.Definitions

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2)

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2)

sNegate :: Sing t -> Sing (Apply NegateSym0 t)

sAbs :: Sing t -> Sing (Apply AbsSym0 t)

sSignum :: Sing t -> Sing (Apply SignumSym0 t)

sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t)

ShowSing Nat => ShowSing Nat

Defined in Data.Type.Natural.Definitions

Methods

showsSingPrec :: Int -> Sing a -> ShowS

POrd Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type Compare arg arg1 :: Ordering

type arg < arg1 :: Bool

type arg <= arg1 :: Bool

type arg > arg1 :: Bool

type arg >= arg1 :: Bool

type Max arg arg1 :: a

type Min arg arg1 :: a

SOrd Nat

Defined in Data.Type.Natural.Definitions

Methods

sCompare :: Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)

(%<) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2)

(%<=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2)

(%>) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2)

(%>=) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2)

sMax :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2)

sMin :: Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2)

SEq Nat => SEq Nat

Defined in Data.Type.Natural.Definitions

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

PEq Nat

Defined in Data.Type.Natural.Definitions

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide Nat => SDecide Nat

Defined in Data.Type.Natural.Definitions

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

IsPeano Nat

Since 0.5.0.0

Defined in Data.Type.Natural

Methods

succOneCong :: Succ (Zero Nat) :~: One Nat

succInj :: (Succ n :~: Succ m) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero Nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m)

plusZeroR :: Sing n -> (n + Zero Nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m)

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat

multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n)

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One Nat) :~: n

multOneL :: Sing n -> (One Nat * n) :~: n

plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero Nat

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat)

predSucc :: Sing n -> Pred (Succ n) :~: n

zeroOrSucc :: Sing n -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat

predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero Nat) :~: n

multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing n

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

PeanoOrder Nat

Defined in Data.Type.Natural

Methods

leqToCmp :: Sing a -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing a -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing a -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing a -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing a -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing a -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT

ltToLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b)

gtToLeq :: Sing a -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a)

ltToSuccLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b)

cmpZero :: Sing a -> Compare (Zero Nat) (Succ a) :~: LT

leqToGT :: Sing a -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero Nat) a :~: EQ) (Compare (Zero Nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero Nat) :~: LT) -> Void

ltRightPredSucc :: Sing a -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing n -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing a -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing n -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing n -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing a -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero Nat <= n)

leqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)

fromLeqView :: LeqView n m -> IsTrue (n <= m)

leqViewRefl :: Sing n -> LeqView n n

viewLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView n m

leqWitness :: Sing n -> Sing m -> IsTrue (n <= m) -> DiffNat n m

leqStep :: Sing n -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m)

leqNeqToSuccLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m)

leqRefl :: Sing n -> IsTrue (n <= n)

leqSuccStepR :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)

leqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)

leqReflexive :: Sing n -> Sing m -> (n :~: m) -> IsTrue (n <= m)

leqTrans :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)

leqAntisymm :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m

plusMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k))

leqZeroElim :: Sing n -> IsTrue (n <= Zero Nat) -> n :~: Zero Nat

plusMonotoneL :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

plusMonotoneR :: Sing n -> Sing m -> Sing l -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l))

plusLeqL :: Sing n -> Sing m -> IsTrue (n <= (n + m))

plusLeqR :: Sing n -> Sing m -> IsTrue (m <= (n + m))

plusCancelLeqR :: Sing n -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m)

plusCancelLeqL :: Sing n -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero Nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero Nat) :~: False

succLeqAbsurd :: Sing n -> IsTrue (S n <= n) -> Void

succLeqAbsurd' :: Sing n -> (S n <= n) :~: False

notLeqToLeq :: (n <= m) ~ False => Sing n -> Sing m -> IsTrue (m <= n)

leqSucc' :: Sing n -> Sing m -> (n <= m) :~: (Succ n <= Succ m)

leqToMin :: Sing n -> Sing m -> IsTrue (n <= m) -> Min n m :~: n

geqToMin :: Sing n -> Sing m -> IsTrue (m <= n) -> Min n m :~: m

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing n -> Sing m -> IsTrue (Min n m <= n)

minLeqR :: Sing n -> Sing m -> IsTrue (Min n m <= m)

minLargest :: Sing l -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m)

leqToMax :: Sing n -> Sing m -> IsTrue (n <= m) -> Max n m :~: m

geqToMax :: Sing n -> Sing m -> IsTrue (m <= n) -> Max n m :~: n

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing n -> Sing m -> IsTrue (m <= Max n m)

maxLeqL :: Sing n -> Sing m -> IsTrue (n <= Max n m)

maxLeast :: Sing l -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l)

leqReversed :: Sing n -> Sing m -> (n <= m) :~: (m >= n)

lneqSuccLeq :: Sing n -> Sing m -> (n < m) :~: (Succ n <= m)

lneqReversed :: Sing n -> Sing m -> (n < m) :~: (m > n)

lneqToLT :: Sing n -> Sing m -> IsTrue (n < m) -> Compare n m :~: LT

ltToLneq :: Sing n -> Sing m -> (Compare n m :~: LT) -> IsTrue (n < m)

lneqZero :: Sing a -> IsTrue (Zero Nat < Succ a)

lneqSucc :: Sing n -> IsTrue (n < Succ n)

succLneqSucc :: Sing n -> Sing m -> (n < m) :~: (Succ n < Succ m)

lneqRightPredSucc :: Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)

lneqSuccStepR :: Sing n -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)

plusStrictMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k))

maxZeroL :: Sing n -> Max (Zero Nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero Nat) :~: n

minZeroL :: Sing n -> Min (Zero Nat) n :~: Zero Nat

minZeroR :: Sing n -> Min n (Zero Nat) :~: Zero Nat

minusSucc :: Sing n -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero Nat) -> Void

minusPlus :: PeanoOrder Nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n

SingI Z

Defined in Data.Type.Natural.Definitions

Methods

sing :: Sing Z

SingI n => SingI (S n :: Nat)

Defined in Data.Type.Natural.Definitions

Methods

sing :: Sing (S n)

SingI n => Bounded (Ordinal (S n))

Defined in Data.Type.Ordinal

Methods

minBound :: Ordinal (S n)

maxBound :: Ordinal (S n)

Eq (Sing n)

Defined in Data.Type.Natural.Core

Methods

(==) :: Sing n -> Sing n -> Bool

(/=) :: Sing n -> Sing n -> Bool

ShowSing Nat => Show (Sing z)

Defined in Data.Type.Natural.Definitions

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

SuppressUnusedWarnings SSym0

Defined in Data.Type.Natural.Definitions

Methods

suppressUnusedWarnings :: ()

type Demote Nat

Defined in Data.Type.Natural.Definitions

type Demote Nat = Nat

data Sing (z :: Nat)

Defined in Data.Type.Natural.Definitions

data Sing (z :: Nat) where

• SZ :: Sing Z
• SS :: Sing (S n)

type FromEnum (a :: Nat)

Defined in Data.Type.Natural.Definitions

type FromEnum (a :: Nat)

type ToEnum a

Defined in Data.Type.Natural.Definitions

type ToEnum a

type Pred (a :: Nat)

Defined in Data.Type.Natural.Definitions

type Pred (a :: Nat)

type Succ (a :: Nat)

Defined in Data.Type.Natural.Definitions

type Succ (a :: Nat)

type Show_ (arg :: Nat)

Defined in Data.Type.Natural.Definitions

type Show_ (arg :: Nat) = Apply (Show__6989586621679675935Sym0 :: TyFun Nat Symbol -> *) arg

type FromInteger a

Defined in Data.Type.Natural.Definitions

type FromInteger a

type Signum (a :: Nat)

Defined in Data.Type.Natural.Definitions

type Signum (a :: Nat)

type Abs (a :: Nat)

Defined in Data.Type.Natural.Definitions

type Abs (a :: Nat)

type Negate (arg :: Nat)

Defined in Data.Type.Natural.Definitions

type Negate (arg :: Nat) = Apply (Negate_6989586621679412401Sym0 :: TyFun Nat Nat -> *) arg

type EnumFromTo (arg :: Nat) (arg1 :: Nat)

Defined in Data.Type.Natural.Definitions

type EnumFromTo (arg :: Nat) (arg1 :: Nat) = Apply (Apply (EnumFromTo_6989586621679845907Sym0 :: TyFun Nat (TyFun Nat [Nat] -> Type) -> *) arg) arg1

type ShowList (arg :: [Nat]) arg1

Defined in Data.Type.Natural.Definitions

type ShowList (arg :: [Nat]) arg1 = Apply (Apply (ShowList_6989586621679675953Sym0 :: TyFun [Nat] (TyFun Symbol Symbol -> Type) -> *) arg) arg1

type (a1 :: Nat) * (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) * (a2 :: Nat)

type (a1 :: Nat) - (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) - (a2 :: Nat)

type (a1 :: Nat) + (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) + (a2 :: Nat)

type Min (a1 :: Nat) (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type Min (a1 :: Nat) (a2 :: Nat)

type Max (a1 :: Nat) (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type Max (a1 :: Nat) (a2 :: Nat)

type (a1 :: Nat) >= (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) >= (a2 :: Nat)

type (a1 :: Nat) > (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) > (a2 :: Nat)

type (a1 :: Nat) <= (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) <= (a2 :: Nat)

type (a1 :: Nat) < (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) < (a2 :: Nat)

type Compare (arg :: Nat) (arg1 :: Nat)

Defined in Data.Type.Natural.Definitions

type Compare (arg :: Nat) (arg1 :: Nat) = Apply (Apply (Compare_6989586621679300505Sym0 :: TyFun Nat (TyFun Nat Ordering -> Type) -> *) arg) arg1

type (x :: Nat) /= (y :: Nat)

Defined in Data.Type.Natural.Definitions

type (x :: Nat) /= (y :: Nat) = Not (x == y)

type (a :: Nat) == (b :: Nat)

Defined in Data.Type.Natural.Definitions

type (a :: Nat) == (b :: Nat)

type Apply SSym0 (l :: Nat)

Defined in Data.Type.Natural.Definitions

type Apply SSym0 (l :: Nat) = S l

type EnumFromThenTo (arg :: Nat) (arg1 :: Nat) (arg2 :: Nat)

Defined in Data.Type.Natural.Definitions

type EnumFromThenTo (arg :: Nat) (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Apply (EnumFromThenTo_6989586621679845937Sym0 :: TyFun Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) -> *) arg) arg1) arg2

type ShowsPrec a1 (a2 :: Nat) a3

Defined in Data.Type.Natural.Definitions

type ShowsPrec a1 (a2 :: Nat) a3

data SSym0 (l :: TyFun Nat Nat)

Instances

SuppressUnusedWarnings SSym0

Defined in Data.Type.Natural.Definitions

Methods

suppressUnusedWarnings :: ()

type Apply SSym0 (l :: Nat)

Defined in Data.Type.Natural.Definitions

type Apply SSym0 (l :: Nat) = S l

type SSym1 (t :: Nat) = S t

type ZSym0 = Z

Singleton type for Nat.

type SNat = (Sing :: Nat -> Type)

data family Sing (a :: k) :: *

The singleton kind-indexed data family.

Instances

Eq (Sing n)

Defined in Data.Type.Natural.Core

Methods

(==) :: Sing n -> Sing n -> Bool

(/=) :: Sing n -> Sing n -> Bool

ShowSing Nat => Show (Sing z)

Defined in Data.Type.Natural.Definitions

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Nat)

Defined in Data.Type.Natural.Definitions

data Sing (z :: Nat) where

• SZ :: Sing Z
• SS :: Sing (S n)

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [a])
• SCons :: Sing (n1 ': n2)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n1 :| n2)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n1 n2 n3)

data Sing (z :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d)) where

• STuple4 :: Sing ((,,,) n1 n2 n3 n4)

data Sing (z :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e)) where

• STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (z :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f)) where

• STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (z :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f, g)) where

• STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

Arithmetic functions and their singletons.

min :: Ord a => a -> a -> a

type family Min (arg :: a) (arg1 :: a) :: a

Instances

type Min (arg1 :: Bool) (arg2 :: Bool)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Bool) (arg2 :: Bool) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Bool (TyFun Bool Bool -> Type) -> *) arg1) arg2

type Min (arg1 :: Ordering) (arg2 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Ordering) (arg2 :: Ordering) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Ordering (TyFun Ordering Ordering -> Type) -> *) arg1) arg2

type Min (arg1 :: Nat) (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg1) arg2

type Min (arg1 :: Symbol) (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type Min (arg1 :: Symbol) (arg2 :: Symbol) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) arg1) arg2

type Min (arg1 :: ()) (arg2 :: ())

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: ()) (arg2 :: ()) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun () (TyFun () () -> Type) -> *) arg1) arg2

type Min (a1 :: Nat) (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type Min (a1 :: Nat) (a2 :: Nat)

type Min (arg1 :: Void) (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Void) (arg2 :: Void) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun Void (TyFun Void Void -> Type) -> *) arg1) arg2

type Min (arg1 :: [a]) (arg2 :: [a])

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: [a]) (arg2 :: [a]) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun [a] (TyFun [a] [a] -> Type) -> *) arg1) arg2

type Min (arg1 :: Maybe a) (arg2 :: Maybe a)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Maybe a) (arg2 :: Maybe a) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (Maybe a) (TyFun (Maybe a) (Maybe a) -> Type) -> *) arg1) arg2

type Min (arg1 :: NonEmpty a) (arg2 :: NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: NonEmpty a) (arg2 :: NonEmpty a) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (NonEmpty a) (TyFun (NonEmpty a) (NonEmpty a) -> Type) -> *) arg1) arg2

type Min (arg1 :: Either a b) (arg2 :: Either a b)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Either a b) (arg2 :: Either a b) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (Either a b) (TyFun (Either a b) (Either a b) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b)) (arg2 :: (a, b))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b)) (arg2 :: (a, b)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b) (TyFun (a, b) (a, b) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b, c)) (arg2 :: (a, b, c))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b, c)) (arg2 :: (a, b, c)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b, c) (TyFun (a, b, c) (a, b, c) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b, c, d) (TyFun (a, b, c, d) (a, b, c, d) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b, c, d, e) (TyFun (a, b, c, d, e) (a, b, c, d, e) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b, c, d, e, f) (TyFun (a, b, c, d, e, f) (a, b, c, d, e, f) -> Type) -> *) arg1) arg2

type Min (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g)) = Apply (Apply (Min_6989586621679300703Sym0 :: TyFun (a, b, c, d, e, f, g) (TyFun (a, b, c, d, e, f, g) (a, b, c, d, e, f, g) -> Type) -> *) arg1) arg2

sMin :: SOrd a => Sing t1 -> Sing t2 -> Sing (Apply (Apply (MinSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2)

max :: Ord a => a -> a -> a

type family Max (arg :: a) (arg1 :: a) :: a

Instances

type Max (arg1 :: Bool) (arg2 :: Bool)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Bool) (arg2 :: Bool) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Bool (TyFun Bool Bool -> Type) -> *) arg1) arg2

type Max (arg1 :: Ordering) (arg2 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Ordering) (arg2 :: Ordering) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Ordering (TyFun Ordering Ordering -> Type) -> *) arg1) arg2

type Max (arg1 :: Nat) (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Nat) (arg2 :: Nat) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Nat (TyFun Nat Nat -> Type) -> *) arg1) arg2

type Max (arg1 :: Symbol) (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type Max (arg1 :: Symbol) (arg2 :: Symbol) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Symbol (TyFun Symbol Symbol -> Type) -> *) arg1) arg2

type Max (arg1 :: ()) (arg2 :: ())

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: ()) (arg2 :: ()) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun () (TyFun () () -> Type) -> *) arg1) arg2

type Max (a1 :: Nat) (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type Max (a1 :: Nat) (a2 :: Nat)

type Max (arg1 :: Void) (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Void) (arg2 :: Void) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun Void (TyFun Void Void -> Type) -> *) arg1) arg2

type Max (arg1 :: [a]) (arg2 :: [a])

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: [a]) (arg2 :: [a]) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun [a] (TyFun [a] [a] -> Type) -> *) arg1) arg2

type Max (arg1 :: Maybe a) (arg2 :: Maybe a)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Maybe a) (arg2 :: Maybe a) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (Maybe a) (TyFun (Maybe a) (Maybe a) -> Type) -> *) arg1) arg2

type Max (arg1 :: NonEmpty a) (arg2 :: NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: NonEmpty a) (arg2 :: NonEmpty a) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (NonEmpty a) (TyFun (NonEmpty a) (NonEmpty a) -> Type) -> *) arg1) arg2

type Max (arg1 :: Either a b) (arg2 :: Either a b)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Either a b) (arg2 :: Either a b) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (Either a b) (TyFun (Either a b) (Either a b) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b)) (arg2 :: (a, b))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b)) (arg2 :: (a, b)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b) (TyFun (a, b) (a, b) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b, c)) (arg2 :: (a, b, c))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b, c)) (arg2 :: (a, b, c)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b, c) (TyFun (a, b, c) (a, b, c) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b, c, d)) (arg2 :: (a, b, c, d)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b, c, d) (TyFun (a, b, c, d) (a, b, c, d) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b, c, d, e)) (arg2 :: (a, b, c, d, e)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b, c, d, e) (TyFun (a, b, c, d, e) (a, b, c, d, e) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b, c, d, e, f)) (arg2 :: (a, b, c, d, e, f)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b, c, d, e, f) (TyFun (a, b, c, d, e, f) (a, b, c, d, e, f) -> Type) -> *) arg1) arg2

type Max (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: (a, b, c, d, e, f, g)) (arg2 :: (a, b, c, d, e, f, g)) = Apply (Apply (Max_6989586621679300670Sym0 :: TyFun (a, b, c, d, e, f, g) (TyFun (a, b, c, d, e, f, g) (a, b, c, d, e, f, g) -> Type) -> *) arg1) arg2

sMax :: SOrd a => Sing t1 -> Sing t2 -> Sing (Apply (Apply (MaxSym0 :: TyFun a (TyFun a a -> Type) -> *) t1) t2)

data MinSym0 (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *

Instances

SuppressUnusedWarnings (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162) = MinSym1 l

data MinSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *

Instances

SuppressUnusedWarnings (MinSym1 :: a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MinSym1 l1 :: TyFun a a -> *) (l2 :: a) = Min l1 l2

type MinSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Min t t1

data MaxSym0 (l :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type)) :: forall a6989586621679299162. TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *

Instances

SuppressUnusedWarnings (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym0 :: TyFun a6989586621679299162 (TyFun a6989586621679299162 a6989586621679299162 -> Type) -> *) (l :: a6989586621679299162) = MaxSym1 l

data MaxSym1 (l :: a6989586621679299162) (l1 :: TyFun a6989586621679299162 a6989586621679299162) :: forall a6989586621679299162. a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *

Instances

SuppressUnusedWarnings (MaxSym1 :: a6989586621679299162 -> TyFun a6989586621679299162 a6989586621679299162 -> *)

Defined in Data.Singletons.Prelude.Ord

Methods

suppressUnusedWarnings :: ()

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Ord

type Apply (MaxSym1 l1 :: TyFun a a -> *) (l2 :: a) = Max l1 l2

type MaxSym2 (t :: a6989586621679299162) (t1 :: a6989586621679299162) = Max t t1

type family (arg :: a) + (arg1 :: a) :: a

Instances

type (a :: Nat) + (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) + (b :: Nat) = a + b

type (a1 :: Nat) + (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) + (a2 :: Nat)

data (+@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *

Instances

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326)

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326) = (+@#@$$) l

data (l :: a6989586621679412326) +@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *

Instances

SuppressUnusedWarnings ((+@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

type (+@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t + t1

(%+) :: SNum a => Sing t1 -> Sing t2 -> Sing (Apply (Apply ((+@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 6

type family (arg :: a) * (arg1 :: a) :: a

Instances

type (a :: Nat) * (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) * (b :: Nat) = a * b

type (a1 :: Nat) * (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) * (a2 :: Nat)

data (*@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *

Instances

SuppressUnusedWarnings ((*@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326)

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326) = (*@#@$$) l

data (l :: a6989586621679412326) *@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *

Instances

SuppressUnusedWarnings ((*@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((*@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 * l2

type (*@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t * t1

(%*) :: SNum a => Sing t1 -> Sing t2 -> Sing (Apply (Apply ((*@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 7

type family (arg :: a) - (arg1 :: a) :: a

Instances

type (a :: Nat) - (b :: Nat)

Defined in Data.Singletons.Prelude.Num

type (a :: Nat) - (b :: Nat) = a - b

type (a1 :: Nat) - (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) - (a2 :: Nat)

type family (a :: Nat) ** (a :: Nat) :: Nat where ...

Equations

_ ** Z = Apply SSym0 ZSym0

n ** (S m) = Apply (Apply (*@#@$) (Apply (Apply (**@#@$) n) m)) n

(%**) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (**@#@$) t) t :: Nat)

data (-@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *

Instances

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326)

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326) = (-@#@$$) l

data (l :: a6989586621679412326) -@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *

Instances

SuppressUnusedWarnings ((-@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *)

Defined in Data.Singletons.Prelude.Num

Methods

suppressUnusedWarnings :: ()

type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a)

Defined in Data.Singletons.Prelude.Num

type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

type (-@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t - t1

(%-) :: SNum a => Sing t1 -> Sing t2 -> Sing (Apply (Apply ((-@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 6

Type-level predicate & judgements

data Leq (n :: Nat) (m :: Nat) where

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m

SuccLeqSucc :: Leq n m -> Leq (S n) (S m)

type family (arg :: a) <= (arg1 :: a) :: Bool

Instances

type (arg1 :: Bool) <= (arg2 :: Bool)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Bool) <= (arg2 :: Bool) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Bool (TyFun Bool Bool -> Type) -> *) arg1) arg2

type (arg1 :: Ordering) <= (arg2 :: Ordering)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Ordering) <= (arg2 :: Ordering) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Ordering (TyFun Ordering Bool -> Type) -> *) arg1) arg2

type (arg1 :: Nat) <= (arg2 :: Nat)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Nat) <= (arg2 :: Nat) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Nat (TyFun Nat Bool -> Type) -> *) arg1) arg2

type (arg1 :: Symbol) <= (arg2 :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

type (arg1 :: Symbol) <= (arg2 :: Symbol) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Symbol (TyFun Symbol Bool -> Type) -> *) arg1) arg2

type (arg1 :: ()) <= (arg2 :: ())

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: ()) <= (arg2 :: ()) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun () (TyFun () Bool -> Type) -> *) arg1) arg2

type (a1 :: Nat) <= (a2 :: Nat)

Defined in Data.Type.Natural.Definitions

type (a1 :: Nat) <= (a2 :: Nat)

type (arg1 :: Void) <= (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) <= (arg2 :: Void) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun Void (TyFun Void Bool -> Type) -> *) arg1) arg2

type (arg1 :: [a]) <= (arg2 :: [a])

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: [a]) <= (arg2 :: [a]) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun [a] (TyFun [a] Bool -> Type) -> *) arg1) arg2

type (arg1 :: Maybe a) <= (arg2 :: Maybe a)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Maybe a) <= (arg2 :: Maybe a) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (Maybe a) (TyFun (Maybe a) Bool -> Type) -> *) arg1) arg2

type (arg1 :: NonEmpty a) <= (arg2 :: NonEmpty a)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: NonEmpty a) <= (arg2 :: NonEmpty a) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (NonEmpty a) (TyFun (NonEmpty a) Bool -> Type) -> *) arg1) arg2

type (arg1 :: Either a b) <= (arg2 :: Either a b)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Either a b) <= (arg2 :: Either a b) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (Either a b) (TyFun (Either a b) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b)) <= (arg2 :: (a, b))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b)) <= (arg2 :: (a, b)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b) (TyFun (a, b) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b, c)) <= (arg2 :: (a, b, c))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b, c)) <= (arg2 :: (a, b, c)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b, c) (TyFun (a, b, c) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b, c, d)) <= (arg2 :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b, c, d)) <= (arg2 :: (a, b, c, d)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b, c, d) (TyFun (a, b, c, d) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b, c, d, e)) <= (arg2 :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b, c, d, e)) <= (arg2 :: (a, b, c, d, e)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b, c, d, e) (TyFun (a, b, c, d, e) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b, c, d, e, f)) <= (arg2 :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b, c, d, e, f)) <= (arg2 :: (a, b, c, d, e, f)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b, c, d, e, f) (TyFun (a, b, c, d, e, f) Bool -> Type) -> *) arg1) arg2

type (arg1 :: (a, b, c, d, e, f, g)) <= (arg2 :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: (a, b, c, d, e, f, g)) <= (arg2 :: (a, b, c, d, e, f, g)) = Apply (Apply (TFHelper_6989586621679300571Sym0 :: TyFun (a, b, c, d, e, f, g) (TyFun (a, b, c, d, e, f, g) Bool -> Type) -> *) arg1) arg2

type LeqInstance n m = IsTrue (n <= m)

boolToPropLeq :: (n <= m) ~ True => SNat n -> SNat m -> Leq n m

boolToClassLeq :: (n <= m) ~ True => SNat n -> SNat m -> LeqInstance n m

propToClassLeq :: Leq n m -> LeqInstance n m

propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m

Conversion functions

natToInt :: Integral n => Nat -> n

Convert Nat into normal integers.

intToNat :: (Integral a, Ord a) => a -> Nat

Convert integral numbers into Nat

sNatToInt :: Num n => SNat x -> n

Convert 'SNat n' into normal integers.

Quasi quotes for natural numbers

nat :: QuasiQuoter

Quotesi-quoter for Nat. This can be used for an expression, pattern and type.

for example: sing :: SNat ([nat| 2 |] :+ [nat| 5 |])

snat :: QuasiQuoter

Quotesi-quoter for SNat. This can be used for an expression.

For example: [snat|12|] %+ [snat| 5 |].

Properties of natural numbers

class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where

Minimal complete definition

succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction

Methods

succOneCong :: Succ (Zero nat) :~: One nat

succInj :: (Succ n :~: Succ (m :: nat)) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ (m :: nat)) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void

induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat)

plusZeroR :: Sing n -> (n + Zero nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat)

plusComm :: Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n)

plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero nat * n) :~: Zero nat

multSuccL :: Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero nat) :~: Zero nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat))

multComm :: Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One nat) :~: n

multOneL :: Sing n -> (One nat * n) :~: n

plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero nat

multAssoc :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One nat)

predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat)

zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> n :~: Zero nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> m :~: Zero nat

predUnique :: Sing (n :: nat) -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero nat) :~: n

multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat)

toNatural :: Sing (n :: nat) -> Natural

fromNatural :: Natural -> SomeSing nat

Instances

IsPeano Nat

Defined in Data.Type.Natural.Builtin

Methods

succOneCong :: Succ (Zero Nat) :~: One Nat

succInj :: (Succ n :~: Succ m) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero Nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m)

plusZeroR :: Sing n -> (n + Zero Nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m)

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat

multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n)

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One Nat) :~: n

multOneL :: Sing n -> (One Nat * n) :~: n

plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero Nat

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat)

predSucc :: Sing n -> Pred (Succ n) :~: n

zeroOrSucc :: Sing n -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat

predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero Nat) :~: n

multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing n

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

IsPeano Nat

Since 0.5.0.0

Defined in Data.Type.Natural

Methods

succOneCong :: Succ (Zero Nat) :~: One Nat

succInj :: (Succ n :~: Succ m) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero Nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m)

plusZeroR :: Sing n -> (n + Zero Nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m)

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat

multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n)

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One Nat) :~: n

multOneL :: Sing n -> (One Nat * n) :~: n

plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero Nat

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat)

predSucc :: Sing n -> Pred (Succ n) :~: n

zeroOrSucc :: Sing n -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat

predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero Nat) :~: n

multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing n

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

plusCong :: (n :~: m) -> (n' :~: m') -> (n + n') :~: (m + m')

plusCongR :: Sing k -> (n :~: m) -> (k + n) :~: (k + m)

plusCongL :: (n :~: m) -> Sing k -> (n + k) :~: (m + k)

snEqZAbsurd :: SingI n => (S n :~: Z) -> a

plusInjectiveL :: SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l

plusInjectiveR :: SNat n -> SNat m -> SNat l -> ((n + l) :~: (m + l)) -> n :~: m

multCongL :: (n :~: m) -> Sing k -> (n * k) :~: (m * k)

multCongR :: Sing k -> (n :~: m) -> (k * n) :~: (k * m)

multCong :: (n :~: m) -> (l :~: k) -> (n * l) :~: (m * k)

plusMinusEqL :: SNat n -> SNat m -> ((n + m) - m) :~: n

plusNeutralR :: SNat n -> SNat m -> ((n + m) :~: n) -> m :~: Z

plusNeutralL :: SNat n -> SNat m -> ((n + m) :~: m) -> n :~: Z

Properties of ordering Leq

class (SOrd nat, IsPeano nat) => PeanoOrder nat where

Minimal complete definition

(succLeqToLT, cmpZero, leqRefl | leqZero, leqSucc, viewLeq | leqWitness, leqStep), eqlCmpEQ, ltToLeq, eqToRefl, flipCompare, leqToCmp, leqReversed, lneqSuccLeq, lneqReversed, (leqToMin, geqToMin | minLeqL, minLeqR, minLargest), (leqToMax, geqToMax | maxLeqL, maxLeqR, maxLeast)

Methods

leqToCmp :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing (a :: nat) -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing (a :: nat) -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing (a :: nat) -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT

ltToLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b)

gtToLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a)

ltToSuccLeq :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b)

cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: LT

leqToGT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: EQ) (Compare (Zero nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero nat) :~: LT) -> Void

ltRightPredSucc :: Sing (a :: nat) -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing (n :: nat) -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing (n :: nat) -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing (n :: nat) -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing (a :: nat) -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero nat <= n)

leqSucc :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)

fromLeqView :: LeqView (n :: nat) m -> IsTrue (n <= m)

leqViewRefl :: Sing (n :: nat) -> LeqView n n

viewLeq :: forall n m. Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> LeqView n m

leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> DiffNat n m

leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m)

leqNeqToSuccLeq :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m)

leqRefl :: Sing (n :: nat) -> IsTrue (n <= n)

leqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)

leqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)

leqReflexive :: Sing (n :: nat) -> Sing m -> (n :~: m) -> IsTrue (n <= m)

leqTrans :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)

leqAntisymm :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m

plusMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k))

leqZeroElim :: Sing n -> IsTrue (n <= Zero nat) -> n :~: Zero nat

plusMonotoneL :: Sing (n :: nat) -> Sing m -> Sing (l :: nat) -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

plusMonotoneR :: Sing n -> Sing m -> Sing (l :: nat) -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l))

plusLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= (n + m))

plusLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= (n + m))

plusCancelLeqR :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m)

plusCancelLeqL :: Sing (n :: nat) -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero nat) :~: False

succLeqAbsurd :: Sing (n :: nat) -> IsTrue (S n <= n) -> Void

succLeqAbsurd' :: Sing (n :: nat) -> (S n <= n) :~: False

notLeqToLeq :: (n <= m) ~ False => Sing (n :: nat) -> Sing m -> IsTrue (m <= n)

leqSucc' :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (Succ n <= Succ m)

leqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Min n m :~: n

geqToMin :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Min n m :~: m

minComm :: Sing (n :: nat) -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= n)

minLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (Min n m <= m)

minLargest :: Sing (l :: nat) -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m)

leqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (n <= m) -> Max n m :~: m

geqToMax :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> Max n m :~: n

maxComm :: Sing (n :: nat) -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing (n :: nat) -> Sing m -> IsTrue (m <= Max n m)

maxLeqL :: Sing (n :: nat) -> Sing m -> IsTrue (n <= Max n m)

maxLeast :: Sing (l :: nat) -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l)

leqReversed :: Sing (n :: nat) -> Sing m -> (n <= m) :~: (m >= n)

lneqSuccLeq :: Sing (n :: nat) -> Sing m -> (n < m) :~: (Succ n <= m)

lneqReversed :: Sing (n :: nat) -> Sing m -> (n < m) :~: (m > n)

lneqToLT :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m) -> Compare n m :~: LT

ltToLneq :: Sing (n :: nat) -> Sing (m :: nat) -> (Compare n m :~: LT) -> IsTrue (n < m)

lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat < Succ a)

lneqSucc :: Sing (n :: nat) -> IsTrue (n < Succ n)

succLneqSucc :: Sing (n :: nat) -> Sing (m :: nat) -> (n < m) :~: (Succ n < Succ m)

lneqRightPredSucc :: Sing (n :: nat) -> Sing (m :: nat) -> IsTrue (n < m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)

lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)

plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k))

maxZeroL :: Sing n -> Max (Zero nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero nat) :~: n

minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat

minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat

minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero nat) -> Void

minusPlus :: forall (n :: nat) m. PeanoOrder nat => Sing (n :: nat) -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n

Instances

PeanoOrder Nat

Defined in Data.Type.Natural.Builtin

Methods

leqToCmp :: Sing a -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing a -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing a -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing a -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing a -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing a -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT

ltToLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b)

gtToLeq :: Sing a -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a)

ltToSuccLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b)

cmpZero :: Sing a -> Compare (Zero Nat) (Succ a) :~: LT

leqToGT :: Sing a -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero Nat) a :~: EQ) (Compare (Zero Nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero Nat) :~: LT) -> Void

ltRightPredSucc :: Sing a -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing n -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing a -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing n -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing n -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing a -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero Nat <= n)

leqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)

fromLeqView :: LeqView n m -> IsTrue (n <= m)

leqViewRefl :: Sing n -> LeqView n n

viewLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView n m

leqWitness :: Sing n -> Sing m -> IsTrue (n <= m) -> DiffNat n m

leqStep :: Sing n -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m)

leqNeqToSuccLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m)

leqRefl :: Sing n -> IsTrue (n <= n)

leqSuccStepR :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)

leqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)

leqReflexive :: Sing n -> Sing m -> (n :~: m) -> IsTrue (n <= m)

leqTrans :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)

leqAntisymm :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m

plusMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k))

leqZeroElim :: Sing n -> IsTrue (n <= Zero Nat) -> n :~: Zero Nat

plusMonotoneL :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

plusMonotoneR :: Sing n -> Sing m -> Sing l -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l))

plusLeqL :: Sing n -> Sing m -> IsTrue (n <= (n + m))

plusLeqR :: Sing n -> Sing m -> IsTrue (m <= (n + m))

plusCancelLeqR :: Sing n -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m)

plusCancelLeqL :: Sing n -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero Nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero Nat) :~: False

succLeqAbsurd :: Sing n -> IsTrue (S n <= n) -> Void

succLeqAbsurd' :: Sing n -> (S n <= n) :~: False

notLeqToLeq :: (n <= m) ~ False => Sing n -> Sing m -> IsTrue (m <= n)

leqSucc' :: Sing n -> Sing m -> (n <= m) :~: (Succ n <= Succ m)

leqToMin :: Sing n -> Sing m -> IsTrue (n <= m) -> Min n m :~: n

geqToMin :: Sing n -> Sing m -> IsTrue (m <= n) -> Min n m :~: m

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing n -> Sing m -> IsTrue (Min n m <= n)

minLeqR :: Sing n -> Sing m -> IsTrue (Min n m <= m)

minLargest :: Sing l -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m)

leqToMax :: Sing n -> Sing m -> IsTrue (n <= m) -> Max n m :~: m

geqToMax :: Sing n -> Sing m -> IsTrue (m <= n) -> Max n m :~: n

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing n -> Sing m -> IsTrue (m <= Max n m)

maxLeqL :: Sing n -> Sing m -> IsTrue (n <= Max n m)

maxLeast :: Sing l -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l)

leqReversed :: Sing n -> Sing m -> (n <= m) :~: (m >= n)

lneqSuccLeq :: Sing n -> Sing m -> (n < m) :~: (Succ n <= m)

lneqReversed :: Sing n -> Sing m -> (n < m) :~: (m > n)

lneqToLT :: Sing n -> Sing m -> IsTrue (n < m) -> Compare n m :~: LT

ltToLneq :: Sing n -> Sing m -> (Compare n m :~: LT) -> IsTrue (n < m)

lneqZero :: Sing a -> IsTrue (Zero Nat < Succ a)

lneqSucc :: Sing n -> IsTrue (n < Succ n)

succLneqSucc :: Sing n -> Sing m -> (n < m) :~: (Succ n < Succ m)

lneqRightPredSucc :: Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)

lneqSuccStepR :: Sing n -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)

plusStrictMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k))

maxZeroL :: Sing n -> Max (Zero Nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero Nat) :~: n

minZeroL :: Sing n -> Min (Zero Nat) n :~: Zero Nat

minZeroR :: Sing n -> Min n (Zero Nat) :~: Zero Nat

minusSucc :: Sing n -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero Nat) -> Void

minusPlus :: PeanoOrder Nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n

PeanoOrder Nat

Defined in Data.Type.Natural

Methods

leqToCmp :: Sing a -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing a -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing a -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing a -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing a -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing a -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT

ltToLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b)

gtToLeq :: Sing a -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a)

ltToSuccLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b)

cmpZero :: Sing a -> Compare (Zero Nat) (Succ a) :~: LT

leqToGT :: Sing a -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero Nat) a :~: EQ) (Compare (Zero Nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero Nat) :~: LT) -> Void

ltRightPredSucc :: Sing a -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing n -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing a -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing n -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing n -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing a -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero Nat <= n)

leqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)

fromLeqView :: LeqView n m -> IsTrue (n <= m)

leqViewRefl :: Sing n -> LeqView n n

viewLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView n m

leqWitness :: Sing n -> Sing m -> IsTrue (n <= m) -> DiffNat n m

leqStep :: Sing n -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m)

leqNeqToSuccLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m)

leqRefl :: Sing n -> IsTrue (n <= n)

leqSuccStepR :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)

leqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)

leqReflexive :: Sing n -> Sing m -> (n :~: m) -> IsTrue (n <= m)

leqTrans :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)

leqAntisymm :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m

plusMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k))

leqZeroElim :: Sing n -> IsTrue (n <= Zero Nat) -> n :~: Zero Nat

plusMonotoneL :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

plusMonotoneR :: Sing n -> Sing m -> Sing l -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l))

plusLeqL :: Sing n -> Sing m -> IsTrue (n <= (n + m))

plusLeqR :: Sing n -> Sing m -> IsTrue (m <= (n + m))

plusCancelLeqR :: Sing n -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m)

plusCancelLeqL :: Sing n -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero Nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero Nat) :~: False

succLeqAbsurd :: Sing n -> IsTrue (S n <= n) -> Void

succLeqAbsurd' :: Sing n -> (S n <= n) :~: False

notLeqToLeq :: (n <= m) ~ False => Sing n -> Sing m -> IsTrue (m <= n)

leqSucc' :: Sing n -> Sing m -> (n <= m) :~: (Succ n <= Succ m)

leqToMin :: Sing n -> Sing m -> IsTrue (n <= m) -> Min n m :~: n

geqToMin :: Sing n -> Sing m -> IsTrue (m <= n) -> Min n m :~: m

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing n -> Sing m -> IsTrue (Min n m <= n)

minLeqR :: Sing n -> Sing m -> IsTrue (Min n m <= m)

minLargest :: Sing l -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m)

leqToMax :: Sing n -> Sing m -> IsTrue (n <= m) -> Max n m :~: m

geqToMax :: Sing n -> Sing m -> IsTrue (m <= n) -> Max n m :~: n

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing n -> Sing m -> IsTrue (m <= Max n m)

maxLeqL :: Sing n -> Sing m -> IsTrue (n <= Max n m)

maxLeast :: Sing l -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l)

leqReversed :: Sing n -> Sing m -> (n <= m) :~: (m >= n)

lneqSuccLeq :: Sing n -> Sing m -> (n < m) :~: (Succ n <= m)

lneqReversed :: Sing n -> Sing m -> (n < m) :~: (m > n)

lneqToLT :: Sing n -> Sing m -> IsTrue (n < m) -> Compare n m :~: LT

ltToLneq :: Sing n -> Sing m -> (Compare n m :~: LT) -> IsTrue (n < m)

lneqZero :: Sing a -> IsTrue (Zero Nat < Succ a)

lneqSucc :: Sing n -> IsTrue (n < Succ n)

succLneqSucc :: Sing n -> Sing m -> (n < m) :~: (Succ n < Succ m)

lneqRightPredSucc :: Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)

lneqSuccStepR :: Sing n -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)

plusStrictMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k))

maxZeroL :: Sing n -> Max (Zero Nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero Nat) :~: n

minZeroL :: Sing n -> Min (Zero Nat) n :~: Zero Nat

minZeroR :: Sing n -> Min n (Zero Nat) :~: Zero Nat

minusSucc :: Sing n -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero Nat) -> Void

minusPlus :: PeanoOrder Nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n

reflToSEqual :: SNat n -> SNat m -> (n :~: m) -> IsTrue (n == m)

sLeqReflexive :: SNat n -> SNat m -> IsTrue (n == m) -> IsTrue (n <= m)

nonSLeqToLT :: (n <= m) ~ False => SNat n -> SNat m -> Compare m n :~: LT

Useful type synonyms and constructors

zero :: Nat

one :: Nat

two :: Nat

three :: Nat

four :: Nat

five :: Nat

six :: Nat

seven :: Nat

eight :: Nat

nine :: Nat

ten :: Nat

eleven :: Nat

twelve :: Nat

thirteen :: Nat

fourteen :: Nat

fifteen :: Nat

sixteen :: Nat

seventeen :: Nat

eighteen :: Nat

nineteen :: Nat

twenty :: Nat

type family Zero :: Nat where ...

Equations

Zero = ZSym0

type family One :: Nat where ...

Equations

One = Apply SSym0 ZeroSym0

type family Two :: Nat where ...

Equations

Two = Apply SSym0 OneSym0

type family Three :: Nat where ...

Equations

Three = Apply SSym0 TwoSym0

type family Four :: Nat where ...

Equations

Four = Apply SSym0 ThreeSym0

type family Five :: Nat where ...

Equations

Five = Apply SSym0 FourSym0

type family Six :: Nat where ...

Equations

Six = Apply SSym0 FiveSym0

type family Seven :: Nat where ...

Equations

Seven = Apply SSym0 SixSym0

type family Eight :: Nat where ...

Equations

Eight = Apply SSym0 SevenSym0

type family Nine :: Nat where ...

Equations

Nine = Apply SSym0 EightSym0

type family Ten :: Nat where ...

Equations

Ten = Apply SSym0 NineSym0

type family Eleven :: Nat where ...

Equations

Eleven = Apply SSym0 TenSym0

type family Twelve :: Nat where ...

Equations

Twelve = Apply SSym0 ElevenSym0

type family Thirteen :: Nat where ...

Equations

Thirteen = Apply SSym0 TwelveSym0

type family Fourteen :: Nat where ...

Equations

Fourteen = Apply SSym0 ThirteenSym0

type family Fifteen :: Nat where ...

Equations

Fifteen = Apply SSym0 FourteenSym0

type family Sixteen :: Nat where ...

Equations

Sixteen = Apply SSym0 FifteenSym0

type family Seventeen :: Nat where ...

Equations

Seventeen = Apply SSym0 SixteenSym0

type family Eighteen :: Nat where ...

Equations

Eighteen = Apply SSym0 SeventeenSym0

type family Nineteen :: Nat where ...

Equations

Nineteen = Apply SSym0 EighteenSym0

type family Twenty :: Nat where ...

Equations

Twenty = Apply SSym0 NineteenSym0

type ZeroSym0 = Zero

type OneSym0 = One

type TwoSym0 = Two

type ThreeSym0 = Three

type FourSym0 = Four

type FiveSym0 = Five

type SixSym0 = Six

type SevenSym0 = Seven

type EightSym0 = Eight

type NineSym0 = Nine

type TenSym0 = Ten

type ElevenSym0 = Eleven

type TwelveSym0 = Twelve

type ThirteenSym0 = Thirteen

type FourteenSym0 = Fourteen

type FifteenSym0 = Fifteen

type SixteenSym0 = Sixteen

type SeventeenSym0 = Seventeen

type EighteenSym0 = Eighteen

type NineteenSym0 = Nineteen

type TwentySym0 = Twenty

sZero :: Sing (ZeroSym0 :: Nat)

sOne :: Sing (OneSym0 :: Nat)

sTwo :: Sing (TwoSym0 :: Nat)

sThree :: Sing (ThreeSym0 :: Nat)

sFour :: Sing (FourSym0 :: Nat)

sFive :: Sing (FiveSym0 :: Nat)

sSix :: Sing (SixSym0 :: Nat)

sSeven :: Sing (SevenSym0 :: Nat)

sEight :: Sing (EightSym0 :: Nat)

sNine :: Sing (NineSym0 :: Nat)

sTen :: Sing (TenSym0 :: Nat)

sEleven :: Sing (ElevenSym0 :: Nat)

sTwelve :: Sing (TwelveSym0 :: Nat)

sThirteen :: Sing (ThirteenSym0 :: Nat)

sFourteen :: Sing (FourteenSym0 :: Nat)

sFifteen :: Sing (FifteenSym0 :: Nat)

sSixteen :: Sing (SixteenSym0 :: Nat)

sSeventeen :: Sing (SeventeenSym0 :: Nat)

sEighteen :: Sing (EighteenSym0 :: Nat)

sNineteen :: Sing (NineteenSym0 :: Nat)

sTwenty :: Sing (TwentySym0 :: Nat)

n0 :: Nat

n1 :: Nat

n2 :: Nat

n3 :: Nat

n4 :: Nat

n5 :: Nat

n6 :: Nat

n7 :: Nat

n8 :: Nat

n9 :: Nat

n10 :: Nat

n11 :: Nat

n12 :: Nat

n13 :: Nat

n14 :: Nat

n15 :: Nat

n16 :: Nat

n17 :: Nat

n18 :: Nat

n19 :: Nat

n20 :: Nat

type family N0 :: Nat where ...

Equations

N0 = ZeroSym0

type family N1 :: Nat where ...

Equations

N1 = OneSym0

type family N2 :: Nat where ...

Equations

N2 = TwoSym0

type family N3 :: Nat where ...

Equations

N3 = ThreeSym0

type family N4 :: Nat where ...

Equations

N4 = FourSym0

type family N5 :: Nat where ...

Equations

N5 = FiveSym0

type family N6 :: Nat where ...

Equations

N6 = SixSym0

type family N7 :: Nat where ...

Equations

N7 = SevenSym0

type family N8 :: Nat where ...

Equations

N8 = EightSym0

type family N9 :: Nat where ...

Equations

N9 = NineSym0

type family N10 :: Nat where ...

Equations

N10 = TenSym0

type family N11 :: Nat where ...

Equations

N11 = ElevenSym0

type family N12 :: Nat where ...

Equations

N12 = TwelveSym0

type family N13 :: Nat where ...

Equations

N13 = ThirteenSym0

type family N14 :: Nat where ...

Equations

N14 = FourteenSym0

type family N15 :: Nat where ...

Equations

N15 = FifteenSym0

type family N16 :: Nat where ...

Equations

N16 = SixteenSym0

type family N17 :: Nat where ...

Equations

N17 = SeventeenSym0

type family N18 :: Nat where ...

Equations

N18 = EighteenSym0

type family N19 :: Nat where ...

Equations

N19 = NineteenSym0

type family N20 :: Nat where ...

Equations

N20 = TwentySym0

type N0Sym0 = N0

type N1Sym0 = N1

type N2Sym0 = N2

type N3Sym0 = N3

type N4Sym0 = N4

type N5Sym0 = N5

type N6Sym0 = N6

type N7Sym0 = N7

type N8Sym0 = N8

type N9Sym0 = N9

type N10Sym0 = N10

type N11Sym0 = N11

type N12Sym0 = N12

type N13Sym0 = N13

type N14Sym0 = N14

type N15Sym0 = N15

type N16Sym0 = N16

type N17Sym0 = N17

type N18Sym0 = N18

type N19Sym0 = N19

type N20Sym0 = N20

sN0 :: Sing (N0Sym0 :: Nat)

sN1 :: Sing (N1Sym0 :: Nat)

sN2 :: Sing (N2Sym0 :: Nat)

sN3 :: Sing (N3Sym0 :: Nat)

sN4 :: Sing (N4Sym0 :: Nat)

sN5 :: Sing (N5Sym0 :: Nat)

sN6 :: Sing (N6Sym0 :: Nat)

sN7 :: Sing (N7Sym0 :: Nat)

sN8 :: Sing (N8Sym0 :: Nat)

sN9 :: Sing (N9Sym0 :: Nat)

sN10 :: Sing (N10Sym0 :: Nat)

sN11 :: Sing (N11Sym0 :: Nat)

sN12 :: Sing (N12Sym0 :: Nat)

sN13 :: Sing (N13Sym0 :: Nat)

sN14 :: Sing (N14Sym0 :: Nat)

sN15 :: Sing (N15Sym0 :: Nat)

sN16 :: Sing (N16Sym0 :: Nat)

sN17 :: Sing (N17Sym0 :: Nat)

sN18 :: Sing (N18Sym0 :: Nat)

sN19 :: Sing (N19Sym0 :: Nat)

sN20 :: Sing (N20Sym0 :: Nat)

Orphan instances

IsPeano Nat

Since 0.5.0.0

Methods

succOneCong :: Succ (Zero Nat) :~: One Nat

succInj :: (Succ n :~: Succ m) -> n :~: m

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m

succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void

induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k

plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n

plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m

plusZeroL :: Sing n -> (Zero Nat + n) :~: n

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m)

plusZeroR :: Sing n -> (n + Zero Nat) :~: n

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m)

plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n)

plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l))

multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat

multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m)

multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n)

multComm :: Sing n -> Sing m -> (n * m) :~: (m * n)

multOneR :: Sing n -> (n * One Nat) :~: n

multOneL :: Sing n -> (One Nat * n) :~: n

plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l))

multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l))

minusNilpotent :: Sing n -> (n - n) :~: Zero Nat

multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l

plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m

succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n)

succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat)

predSucc :: Sing n -> Pred (Succ n) :~: n

zeroOrSucc :: Sing n -> ZeroOrSucc n

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat

predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m

multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n)

multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m)

minusZero :: Sing n -> (n - Zero Nat) :~: n

multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n

multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l

sPred' :: proxy n -> Sing (Succ n) -> Sing n

toNatural :: Sing n -> Natural

fromNatural :: Natural -> SomeSing Nat

PeanoOrder Nat

Methods

leqToCmp :: Sing a -> Sing b -> IsTrue (a <= b) -> Either (a :~: b) (Compare a b :~: LT)

eqlCmpEQ :: Sing a -> Sing b -> (a :~: b) -> Compare a b :~: EQ

eqToRefl :: Sing a -> Sing b -> (Compare a b :~: EQ) -> a :~: b

flipCompare :: Sing a -> Sing b -> FlipOrdering (Compare a b) :~: Compare b a

ltToNeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> (a :~: b) -> Void

leqNeqToLT :: Sing a -> Sing b -> IsTrue (a <= b) -> ((a :~: b) -> Void) -> Compare a b :~: LT

succLeqToLT :: Sing a -> Sing b -> IsTrue (S a <= b) -> Compare a b :~: LT

ltToLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (a <= b)

gtToLeq :: Sing a -> Sing b -> (Compare a b :~: GT) -> IsTrue (b <= a)

ltToSuccLeq :: Sing a -> Sing b -> (Compare a b :~: LT) -> IsTrue (Succ a <= b)

cmpZero :: Sing a -> Compare (Zero Nat) (Succ a) :~: LT

leqToGT :: Sing a -> Sing b -> IsTrue (Succ b <= a) -> Compare a b :~: GT

cmpZero' :: Sing a -> Either (Compare (Zero Nat) a :~: EQ) (Compare (Zero Nat) a :~: LT)

zeroNoLT :: Sing a -> (Compare a (Zero Nat) :~: LT) -> Void

ltRightPredSucc :: Sing a -> Sing b -> (Compare a b :~: LT) -> b :~: Succ (Pred b)

cmpSucc :: Sing n -> Sing m -> Compare n m :~: Compare (Succ n) (Succ m)

ltSucc :: Sing a -> Compare a (Succ a) :~: LT

cmpSuccStepR :: Sing n -> Sing m -> (Compare n m :~: LT) -> Compare n (Succ m) :~: LT

ltSuccLToLT :: Sing n -> Sing m -> (Compare (Succ n) m :~: LT) -> Compare n m :~: LT

leqToLT :: Sing a -> Sing b -> IsTrue (Succ a <= b) -> Compare a b :~: LT

leqZero :: Sing n -> IsTrue (Zero Nat <= n)

leqSucc :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (Succ n <= Succ m)

fromLeqView :: LeqView n m -> IsTrue (n <= m)

leqViewRefl :: Sing n -> LeqView n n

viewLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> LeqView n m

leqWitness :: Sing n -> Sing m -> IsTrue (n <= m) -> DiffNat n m

leqStep :: Sing n -> Sing m -> Sing l -> ((n + l) :~: m) -> IsTrue (n <= m)

leqNeqToSuccLeq :: Sing n -> Sing m -> IsTrue (n <= m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <= m)

leqRefl :: Sing n -> IsTrue (n <= n)

leqSuccStepR :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (n <= Succ m)

leqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n <= m) -> IsTrue (n <= m)

leqReflexive :: Sing n -> Sing m -> (n :~: m) -> IsTrue (n <= m)

leqTrans :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue (m <= l) -> IsTrue (n <= l)

leqAntisymm :: Sing n -> Sing m -> IsTrue (n <= m) -> IsTrue (m <= n) -> n :~: m

plusMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n <= m) -> IsTrue (l <= k) -> IsTrue ((n + l) <= (m + k))

leqZeroElim :: Sing n -> IsTrue (n <= Zero Nat) -> n :~: Zero Nat

plusMonotoneL :: Sing n -> Sing m -> Sing l -> IsTrue (n <= m) -> IsTrue ((n + l) <= (m + l))

plusMonotoneR :: Sing n -> Sing m -> Sing l -> IsTrue (m <= l) -> IsTrue ((n + m) <= (n + l))

plusLeqL :: Sing n -> Sing m -> IsTrue (n <= (n + m))

plusLeqR :: Sing n -> Sing m -> IsTrue (m <= (n + m))

plusCancelLeqR :: Sing n -> Sing m -> Sing l -> IsTrue ((n + l) <= (m + l)) -> IsTrue (n <= m)

plusCancelLeqL :: Sing n -> Sing m -> Sing l -> IsTrue ((n + m) <= (n + l)) -> IsTrue (m <= l)

succLeqZeroAbsurd :: Sing n -> IsTrue (S n <= Zero Nat) -> Void

succLeqZeroAbsurd' :: Sing n -> (S n <= Zero Nat) :~: False

succLeqAbsurd :: Sing n -> IsTrue (S n <= n) -> Void

succLeqAbsurd' :: Sing n -> (S n <= n) :~: False

notLeqToLeq :: (n <= m) ~ False => Sing n -> Sing m -> IsTrue (m <= n)

leqSucc' :: Sing n -> Sing m -> (n <= m) :~: (Succ n <= Succ m)

leqToMin :: Sing n -> Sing m -> IsTrue (n <= m) -> Min n m :~: n

geqToMin :: Sing n -> Sing m -> IsTrue (m <= n) -> Min n m :~: m

minComm :: Sing n -> Sing m -> Min n m :~: Min m n

minLeqL :: Sing n -> Sing m -> IsTrue (Min n m <= n)

minLeqR :: Sing n -> Sing m -> IsTrue (Min n m <= m)

minLargest :: Sing l -> Sing n -> Sing m -> IsTrue (l <= n) -> IsTrue (l <= m) -> IsTrue (l <= Min n m)

leqToMax :: Sing n -> Sing m -> IsTrue (n <= m) -> Max n m :~: m

geqToMax :: Sing n -> Sing m -> IsTrue (m <= n) -> Max n m :~: n

maxComm :: Sing n -> Sing m -> Max n m :~: Max m n

maxLeqR :: Sing n -> Sing m -> IsTrue (m <= Max n m)

maxLeqL :: Sing n -> Sing m -> IsTrue (n <= Max n m)

maxLeast :: Sing l -> Sing n -> Sing m -> IsTrue (n <= l) -> IsTrue (m <= l) -> IsTrue (Max n m <= l)

leqReversed :: Sing n -> Sing m -> (n <= m) :~: (m >= n)

lneqSuccLeq :: Sing n -> Sing m -> (n < m) :~: (Succ n <= m)

lneqReversed :: Sing n -> Sing m -> (n < m) :~: (m > n)

lneqToLT :: Sing n -> Sing m -> IsTrue (n < m) -> Compare n m :~: LT

ltToLneq :: Sing n -> Sing m -> (Compare n m :~: LT) -> IsTrue (n < m)

lneqZero :: Sing a -> IsTrue (Zero Nat < Succ a)

lneqSucc :: Sing n -> IsTrue (n < Succ n)

succLneqSucc :: Sing n -> Sing m -> (n < m) :~: (Succ n < Succ m)

lneqRightPredSucc :: Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)

lneqSuccStepL :: Sing n -> Sing m -> IsTrue (Succ n < m) -> IsTrue (n < m)

lneqSuccStepR :: Sing n -> Sing m -> IsTrue (n < m) -> IsTrue (n < Succ m)

plusStrictMonotone :: Sing n -> Sing m -> Sing l -> Sing k -> IsTrue (n < m) -> IsTrue (l < k) -> IsTrue ((n + l) < (m + k))

maxZeroL :: Sing n -> Max (Zero Nat) n :~: n

maxZeroR :: Sing n -> Max n (Zero Nat) :~: n

minZeroL :: Sing n -> Min (Zero Nat) n :~: Zero Nat

minZeroR :: Sing n -> Min n (Zero Nat) :~: Zero Nat

minusSucc :: Sing n -> Sing m -> IsTrue (m <= n) -> (Succ n - m) :~: Succ (n - m)

lneqZeroAbsurd :: Sing n -> IsTrue (n < Zero Nat) -> Void

minusPlus :: PeanoOrder Nat => Sing n -> Sing m -> IsTrue (m <= n) -> ((n - m) + m) :~: n