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

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

Methods

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

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

Num Nat

Methods

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

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

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

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat

Ord Nat

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

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

SingKind Nat

Associated Types

type DemoteRep Nat :: *

Methods

fromSing :: Sing Nat a -> DemoteRep Nat

toSing :: DemoteRep Nat -> SomeSing Nat

SEnum Nat

Methods

sSucc :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (SuccSym0 Nat) t0)

sPred :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (PredSym0 Nat) t0)

sToEnum :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (ToEnumSym0 Nat) t0)

sFromEnum :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (FromEnumSym0 Nat) t0)

sEnumFromTo :: Sing Nat t0 -> Sing Nat t1 -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromToSym0 Nat) t0) t1)

sEnumFromThenTo :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat t2 -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (Apply Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) (EnumFromThenToSym0 Nat) t0) t1) t2)

SNum Nat

Methods

(%:+) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t0) t1)

(%:-) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t0) t1)

(%:*) :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:*$) Nat) t0) t1)

sNegate :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t0)

sAbs :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t0)

sSignum :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t0)

sFromInteger :: Sing Nat t0 -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t0)

SOrd Nat

Methods

sCompare :: Sing Nat t0 -> Sing Nat t1 -> Sing Ordering (Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (CompareSym0 Nat) t0) t1)

(%:<) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<$) Nat) t0) t1)

(%:<=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:<=$) Nat) t0) t1)

(%:>) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>$) Nat) t0) t1)

(%:>=) :: Sing Nat t0 -> Sing Nat t1 -> Sing Bool (Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) ((:>=$) Nat) t0) t1)

sMax :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MaxSym0 Nat) t0) t1)

sMin :: Sing Nat t0 -> Sing Nat t1 -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (MinSym0 Nat) t0) t1)

SEq Nat

Methods

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

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

SDecide Nat

Methods

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

SingI Nat Z

Methods

sing :: Sing Z a

SingI Nat n0 => SingI Nat (S n0)

Methods

sing :: Sing (S n0) a

PEnum Nat (Proxy * Nat)

Associated Types

type Succ (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type Pred (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type ToEnum (Proxy * Nat) (arg0 :: Nat) :: a0

type FromEnum (Proxy * Nat) (arg0 :: Proxy * Nat) :: Nat

type EnumFromTo (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: [a0]

type EnumFromThenTo (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) (arg2 :: Proxy * Nat) :: [a0]

PNum Nat (Proxy * Nat)

Associated Types

type ((Proxy * Nat) :+ (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type ((Proxy * Nat) :- (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type ((Proxy * Nat) :* (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: a0

type Negate (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type Abs (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type Signum (Proxy * Nat) (arg0 :: Proxy * Nat) :: a0

type FromInteger (Proxy * Nat) (arg0 :: Nat) :: a0

POrd Nat (Proxy * Nat)

Associated Types

type Compare (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: Ordering

type ((Proxy * Nat) :< (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :<= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :> (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :>= (arg0 :: Proxy * Nat)) (arg1 :: Proxy * Nat) :: Bool

type Max (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0

type Min (Proxy * Nat) (arg0 :: Proxy * Nat) (arg1 :: Proxy * Nat) :: a0

PEq Nat (Proxy * Nat)

Associated Types

type ((Proxy * Nat) :== (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool

type ((Proxy * Nat) :/= (x :: Proxy * Nat)) (y :: Proxy * Nat) :: Bool

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

Methods

minBound :: Ordinal Nat (S n)

maxBound :: Ordinal Nat (S n)

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type DemoteRep Nat

type DemoteRep Nat = Nat

data Sing Nat

data Sing Nat where

• SZ :: Sing Nat z
• SS :: Sing Nat z

type FromEnum Nat a0

type FromEnum Nat a0

type ToEnum Nat a0

type ToEnum Nat a0

type Pred Nat a0

type Pred Nat a0

type Succ Nat a0

type Succ Nat a0

type FromInteger Nat a0

type FromInteger Nat a0

type Signum Nat a0

type Signum Nat a0

type Abs Nat a0

type Abs Nat a0

type Negate Nat arg0

type Negate Nat arg0 = Apply Nat Nat (Negate_1627805905Sym0 Nat) arg0

type EnumFromTo Nat arg0 arg1

type EnumFromTo Nat arg0 arg1 = Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromTo_1627820022Sym0 Nat) arg0) arg1

type (:*) Nat a1 a0

type (:*) Nat a1 a0

type (:-) Nat a1 a0

type (:-) Nat a1 a0

type (:+) Nat a1 a0

type (:+) Nat a1 a0

type Min Nat a1 a0

type Min Nat a1 a0

type Max Nat a1 a0

type Max Nat a1 a0

type (:>=) Nat a1 a0

type (:>=) Nat a1 a0

type (:>) Nat a1 a0

type (:>) Nat a1 a0

type (:<=) Nat a1 a0

type (:<=) Nat a1 a0

type (:<) Nat a1 a0

type (:<) Nat a1 a0

type Compare Nat arg0 arg1

type Compare Nat arg0 arg1 = Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (Compare_1627687955Sym0 Nat) arg0) arg1

type (:/=) Nat x y

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

type (:==) Nat a0 b0

type (:==) Nat a0 b0

type Apply Nat Nat SSym0 l0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type EnumFromThenTo Nat arg0 arg1 arg2

type EnumFromThenTo Nat arg0 arg1 arg2 = Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (Apply Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) (EnumFromThenTo_1627820052Sym0 Nat) arg0) arg1) arg2

type MonomorphicRep Nat (Sing Nat)

type MonomorphicRep Nat (Sing Nat) = Integer

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply Nat Nat SSym0 l0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t

type ZSym0 = Z

Singleton type for Nat.

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

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

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z0
• STrue :: Sing Bool z0

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z0
• SEQ :: Sing Ordering z0
• SGT :: Sing Ordering z0

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z0

data Sing Nat

data Sing Nat where

• SZ :: Sing Nat z
• SS :: Sing Nat z

type MonomorphicRep Nat (Sing Nat)

type MonomorphicRep Nat (Sing Nat) = Integer

type MonomorphicRep Nat (Sing Nat)

type MonomorphicRep Nat (Sing Nat) = Integer

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a0] z0
• SCons :: Sing [a0] z0

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a0) z0
• SJust :: Sing (Maybe a0) z0

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a0) z0

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a0 b0) z0
• SRight :: Sing (Either a0 b0) z0

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a0, b0) z0

data Sing ((~>) k1 k2)

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

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

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a0, b0, c0) z0

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a0, b0, c0, d0) z0

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a0, b0, c0, d0, e0) z0

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a0, b0, c0, d0, e0, f0) z0

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a0, b0, c0, d0, e0, f0, g0) z0

Arithmetic functions and their singletons.

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

type family Min a0 (arg0 :: a0) (arg1 :: a0) :: a0

Instances

type Min Bool arg0 arg1

type Min Bool arg0 arg1 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Min_1627688153Sym0 Bool) arg0) arg1

type Min Ordering arg0 arg1

type Min Ordering arg0 arg1 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Min_1627688153Sym0 Ordering) arg0) arg1

type Min Nat arg0 arg1

type Min Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Min_1627688153Sym0 Nat) arg0) arg1

type Min Symbol arg0 arg1

type Min Symbol arg0 arg1 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Min_1627688153Sym0 Symbol) arg0) arg1

type Min () arg0 arg1

type Min () arg0 arg1 = Apply () () (Apply () (TyFun () () -> Type) (Min_1627688153Sym0 ()) arg0) arg1

type Min Nat a1 a0

type Min Nat a1 a0

type Min [a0] arg0 arg1

type Min [a0] arg0 arg1 = Apply [a0] [a0] (Apply [a0] (TyFun [a0] [a0] -> Type) (Min_1627688153Sym0 [a0]) arg0) arg1

type Min (Maybe a0) arg0 arg1

type Min (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (Maybe a0) (TyFun (Maybe a0) (Maybe a0) -> Type) (Min_1627688153Sym0 (Maybe a0)) arg0) arg1

type Min (NonEmpty a0) arg0 arg1

type Min (NonEmpty a0) arg0 arg1 = Apply (NonEmpty a0) (NonEmpty a0) (Apply (NonEmpty a0) (TyFun (NonEmpty a0) (NonEmpty a0) -> Type) (Min_1627688153Sym0 (NonEmpty a0)) arg0) arg1

type Min (Either a0 b0) arg0 arg1

type Min (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (Either a0 b0) (TyFun (Either a0 b0) (Either a0 b0) -> Type) (Min_1627688153Sym0 (Either a0 b0)) arg0) arg1

type Min (a0, b0) arg0 arg1

type Min (a0, b0) arg0 arg1 = Apply (a0, b0) (a0, b0) (Apply (a0, b0) (TyFun (a0, b0) (a0, b0) -> Type) (Min_1627688153Sym0 (a0, b0)) arg0) arg1

type Min (a0, b0, c0) arg0 arg1

type Min (a0, b0, c0) arg0 arg1 = Apply (a0, b0, c0) (a0, b0, c0) (Apply (a0, b0, c0) (TyFun (a0, b0, c0) (a0, b0, c0) -> Type) (Min_1627688153Sym0 (a0, b0, c0)) arg0) arg1

type Min (a0, b0, c0, d0) arg0 arg1

type Min (a0, b0, c0, d0) arg0 arg1 = Apply (a0, b0, c0, d0) (a0, b0, c0, d0) (Apply (a0, b0, c0, d0) (TyFun (a0, b0, c0, d0) (a0, b0, c0, d0) -> Type) (Min_1627688153Sym0 (a0, b0, c0, d0)) arg0) arg1

type Min (a0, b0, c0, d0, e0) arg0 arg1

type Min (a0, b0, c0, d0, e0) arg0 arg1 = Apply (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) (Apply (a0, b0, c0, d0, e0) (TyFun (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) -> Type) (Min_1627688153Sym0 (a0, b0, c0, d0, e0)) arg0) arg1

type Min (a0, b0, c0, d0, e0, f0) arg0 arg1

type Min (a0, b0, c0, d0, e0, f0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) (Apply (a0, b0, c0, d0, e0, f0) (TyFun (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) -> Type) (Min_1627688153Sym0 (a0, b0, c0, d0, e0, f0)) arg0) arg1

type Min (a0, b0, c0, d0, e0, f0, g0) arg0 arg1

type Min (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) (Apply (a0, b0, c0, d0, e0, f0, g0) (TyFun (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) -> Type) (Min_1627688153Sym0 (a0, b0, c0, d0, e0, f0, g0)) arg0) arg1

sMin :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MinSym0 a0) t0) t1)

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

type family Max a0 (arg0 :: a0) (arg1 :: a0) :: a0

Instances

type Max Bool arg0 arg1

type Max Bool arg0 arg1 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Max_1627688120Sym0 Bool) arg0) arg1

type Max Ordering arg0 arg1

type Max Ordering arg0 arg1 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Max_1627688120Sym0 Ordering) arg0) arg1

type Max Nat arg0 arg1

type Max Nat arg0 arg1 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_1627688120Sym0 Nat) arg0) arg1

type Max Symbol arg0 arg1

type Max Symbol arg0 arg1 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Max_1627688120Sym0 Symbol) arg0) arg1

type Max () arg0 arg1

type Max () arg0 arg1 = Apply () () (Apply () (TyFun () () -> Type) (Max_1627688120Sym0 ()) arg0) arg1

type Max Nat a1 a0

type Max Nat a1 a0

type Max [a0] arg0 arg1

type Max [a0] arg0 arg1 = Apply [a0] [a0] (Apply [a0] (TyFun [a0] [a0] -> Type) (Max_1627688120Sym0 [a0]) arg0) arg1

type Max (Maybe a0) arg0 arg1

type Max (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (Maybe a0) (TyFun (Maybe a0) (Maybe a0) -> Type) (Max_1627688120Sym0 (Maybe a0)) arg0) arg1

type Max (NonEmpty a0) arg0 arg1

type Max (NonEmpty a0) arg0 arg1 = Apply (NonEmpty a0) (NonEmpty a0) (Apply (NonEmpty a0) (TyFun (NonEmpty a0) (NonEmpty a0) -> Type) (Max_1627688120Sym0 (NonEmpty a0)) arg0) arg1

type Max (Either a0 b0) arg0 arg1

type Max (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (Either a0 b0) (TyFun (Either a0 b0) (Either a0 b0) -> Type) (Max_1627688120Sym0 (Either a0 b0)) arg0) arg1

type Max (a0, b0) arg0 arg1

type Max (a0, b0) arg0 arg1 = Apply (a0, b0) (a0, b0) (Apply (a0, b0) (TyFun (a0, b0) (a0, b0) -> Type) (Max_1627688120Sym0 (a0, b0)) arg0) arg1

type Max (a0, b0, c0) arg0 arg1

type Max (a0, b0, c0) arg0 arg1 = Apply (a0, b0, c0) (a0, b0, c0) (Apply (a0, b0, c0) (TyFun (a0, b0, c0) (a0, b0, c0) -> Type) (Max_1627688120Sym0 (a0, b0, c0)) arg0) arg1

type Max (a0, b0, c0, d0) arg0 arg1

type Max (a0, b0, c0, d0) arg0 arg1 = Apply (a0, b0, c0, d0) (a0, b0, c0, d0) (Apply (a0, b0, c0, d0) (TyFun (a0, b0, c0, d0) (a0, b0, c0, d0) -> Type) (Max_1627688120Sym0 (a0, b0, c0, d0)) arg0) arg1

type Max (a0, b0, c0, d0, e0) arg0 arg1

type Max (a0, b0, c0, d0, e0) arg0 arg1 = Apply (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) (Apply (a0, b0, c0, d0, e0) (TyFun (a0, b0, c0, d0, e0) (a0, b0, c0, d0, e0) -> Type) (Max_1627688120Sym0 (a0, b0, c0, d0, e0)) arg0) arg1

type Max (a0, b0, c0, d0, e0, f0) arg0 arg1

type Max (a0, b0, c0, d0, e0, f0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) (Apply (a0, b0, c0, d0, e0, f0) (TyFun (a0, b0, c0, d0, e0, f0) (a0, b0, c0, d0, e0, f0) -> Type) (Max_1627688120Sym0 (a0, b0, c0, d0, e0, f0)) arg0) arg1

type Max (a0, b0, c0, d0, e0, f0, g0) arg0 arg1

type Max (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) (Apply (a0, b0, c0, d0, e0, f0, g0) (TyFun (a0, b0, c0, d0, e0, f0, g0) (a0, b0, c0, d0, e0, f0, g0) -> Type) (Max_1627688120Sym0 (a0, b0, c0, d0, e0, f0, g0)) arg0) arg1

sMax :: SOrd a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) (MaxSym0 a0) t0) t1)

data MinSym0 a1627685643 l0 :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *) (MinSym0 a1627685643)

Methods

suppressUnusedWarnings :: Proxy (MinSym0 a1627685643) t -> ()

type Apply a1627685643 (TyFun a1627685643 a1627685643 -> Type) (MinSym0 a1627685643) l0

type Apply a1627685643 (TyFun a1627685643 a1627685643 -> Type) (MinSym0 a1627685643) l0 = MinSym1 a1627685643 l0

data MinSym1 a1627685643 l0 l1 :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *

Instances

SuppressUnusedWarnings (a1627685643 -> TyFun a1627685643 a1627685643 -> *) (MinSym1 a1627685643)

Methods

suppressUnusedWarnings :: Proxy (MinSym1 a1627685643) t -> ()

type Apply a1627685643 a1627685643 (MinSym1 a1627685643 l0) l1

type Apply a1627685643 a1627685643 (MinSym1 a1627685643 l0) l1 = MinSym2 a1627685643 l0 l1

type MinSym2 a1627685643 t0 t1 = Min a1627685643 t0 t1

data MaxSym0 a1627685643 l0 :: forall a1627685643. TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627685643 (TyFun a1627685643 a1627685643 -> Type) -> *) (MaxSym0 a1627685643)

Methods

suppressUnusedWarnings :: Proxy (MaxSym0 a1627685643) t -> ()

type Apply a1627685643 (TyFun a1627685643 a1627685643 -> Type) (MaxSym0 a1627685643) l0

type Apply a1627685643 (TyFun a1627685643 a1627685643 -> Type) (MaxSym0 a1627685643) l0 = MaxSym1 a1627685643 l0

data MaxSym1 a1627685643 l0 l1 :: forall a1627685643. a1627685643 -> TyFun a1627685643 a1627685643 -> *

Instances

SuppressUnusedWarnings (a1627685643 -> TyFun a1627685643 a1627685643 -> *) (MaxSym1 a1627685643)

Methods

suppressUnusedWarnings :: Proxy (MaxSym1 a1627685643) t -> ()

type Apply a1627685643 a1627685643 (MaxSym1 a1627685643 l0) l1

type Apply a1627685643 a1627685643 (MaxSym1 a1627685643 l0) l1 = MaxSym2 a1627685643 l0 l1

type MaxSym2 a1627685643 t0 t1 = Max a1627685643 t0 t1

type (:+:) n m = n :+ m infixl 6

type family (a0 :+ (arg0 :: a0)) (arg1 :: a0) :: a0

Instances

type (:+) Nat a b

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

type (:+) Nat a1 a0

type (:+) Nat a1 a0

data a1627805829 :+$ l0 :: forall a1627805829. TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *) ((:+$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:+$) a1627805829) t -> ()

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:+$) a1627805829) l0

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:+$) a1627805829) l0 = (:+$$) a1627805829 l0

data (a1627805829 :+$$ l0) l1 :: forall a1627805829. a1627805829 -> TyFun a1627805829 a1627805829 -> *

Instances

SuppressUnusedWarnings (a1627805829 -> TyFun a1627805829 a1627805829 -> *) ((:+$$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:+$$) a1627805829) t -> ()

type Apply a1627805829 a1627805829 ((:+$$) a1627805829 l0) l1

type Apply a1627805829 a1627805829 ((:+$$) a1627805829 l0) l1 = (:+$$$) a1627805829 l0 l1

type (:+$$$) a1627805829 t0 t1 = (:+) a1627805829 t0 t1

(%+) :: SNat n -> SNat m -> SNat (n :+: m) infixl 6

Addition for singleton numbers.

(%:+) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:+$) a0) t0) t1)

type family (a0 :* (arg0 :: a0)) (arg1 :: a0) :: a0

Instances

type (:*) Nat a b

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

type (:*) Nat a1 a0

type (:*) Nat a1 a0

type (:*:) n m = n :* m infixl 7

Type-level multiplication.

data a1627805829 :*$ l0 :: forall a1627805829. TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *) ((:*$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:*$) a1627805829) t -> ()

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:*$) a1627805829) l0

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:*$) a1627805829) l0 = (:*$$) a1627805829 l0

data (a1627805829 :*$$ l0) l1 :: forall a1627805829. a1627805829 -> TyFun a1627805829 a1627805829 -> *

Instances

SuppressUnusedWarnings (a1627805829 -> TyFun a1627805829 a1627805829 -> *) ((:*$$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:*$$) a1627805829) t -> ()

type Apply a1627805829 a1627805829 ((:*$$) a1627805829 l0) l1

type Apply a1627805829 a1627805829 ((:*$$) a1627805829 l0) l1 = (:*$$$) a1627805829 l0 l1

type (:*$$$) a1627805829 t0 t1 = (:*) a1627805829 t0 t1

(%:*) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:*$) a0) t0) t1)

(%*) :: SNat n -> SNat m -> SNat (n :*: m) infixl 7

Multiplication for singleton numbers.

type (:-:) n m = n :- m infixl 6

type family (a0 :- (arg0 :: a0)) (arg1 :: a0) :: a0

Instances

type (:-) Nat a b

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

type (:-) Nat a1 a0

type (:-) Nat a1 a0

type (:**:) n m = n :** m

Type-level exponentiation.

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

Equations

_z_1627480145 :** Z = Apply SSym0 ZSym0

n :** (S m) = Apply (Apply (:*$) (Apply (Apply (:**$) n) m)) n

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

(%**) :: SNat n -> SNat m -> SNat (n :**: m)

Exponentiation for singleton numbers.

data a1627805829 :-$ l0 :: forall a1627805829. TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *

Instances

SuppressUnusedWarnings (TyFun a1627805829 (TyFun a1627805829 a1627805829 -> Type) -> *) ((:-$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:-$) a1627805829) t -> ()

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:-$) a1627805829) l0

type Apply a1627805829 (TyFun a1627805829 a1627805829 -> Type) ((:-$) a1627805829) l0 = (:-$$) a1627805829 l0

data (a1627805829 :-$$ l0) l1 :: forall a1627805829. a1627805829 -> TyFun a1627805829 a1627805829 -> *

Instances

SuppressUnusedWarnings (a1627805829 -> TyFun a1627805829 a1627805829 -> *) ((:-$$) a1627805829)

Methods

suppressUnusedWarnings :: Proxy ((:-$$) a1627805829) t -> ()

type Apply a1627805829 a1627805829 ((:-$$) a1627805829 l0) l1

type Apply a1627805829 a1627805829 ((:-$$) a1627805829 l0) l1 = (:-$$$) a1627805829 l0 l1

type (:-$$$) a1627805829 t0 t1 = (:-) a1627805829 t0 t1

(%:-) :: SNum a0 => forall t0 t1. Sing a0 t0 -> Sing a0 t1 -> Sing a0 (Apply a0 a0 (Apply a0 (TyFun a0 a0 -> Type) ((:-$) a0) t0) t1)

(%-) :: (m :<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m) infixl 6

Type-level predicate & judgements

data Leq n m where

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m

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

type family (a0 :<= (arg0 :: a0)) (arg1 :: a0) :: Bool

Instances

type (:<=) Bool arg0 arg1

type (:<=) Bool arg0 arg1 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (TFHelper_1627688021Sym0 Bool) arg0) arg1

type (:<=) Ordering arg0 arg1

type (:<=) Ordering arg0 arg1 = Apply Ordering Bool (Apply Ordering (TyFun Ordering Bool -> Type) (TFHelper_1627688021Sym0 Ordering) arg0) arg1

type (:<=) Nat arg0 arg1

type (:<=) Nat arg0 arg1 = Apply Nat Bool (Apply Nat (TyFun Nat Bool -> Type) (TFHelper_1627688021Sym0 Nat) arg0) arg1

type (:<=) Symbol arg0 arg1

type (:<=) Symbol arg0 arg1 = Apply Symbol Bool (Apply Symbol (TyFun Symbol Bool -> Type) (TFHelper_1627688021Sym0 Symbol) arg0) arg1

type (:<=) () arg0 arg1

type (:<=) () arg0 arg1 = Apply () Bool (Apply () (TyFun () Bool -> Type) (TFHelper_1627688021Sym0 ()) arg0) arg1

type (:<=) Nat a1 a0

type (:<=) Nat a1 a0

type (:<=) [a0] arg0 arg1

type (:<=) [a0] arg0 arg1 = Apply [a0] Bool (Apply [a0] (TyFun [a0] Bool -> Type) (TFHelper_1627688021Sym0 [a0]) arg0) arg1

type (:<=) (Maybe a0) arg0 arg1

type (:<=) (Maybe a0) arg0 arg1 = Apply (Maybe a0) Bool (Apply (Maybe a0) (TyFun (Maybe a0) Bool -> Type) (TFHelper_1627688021Sym0 (Maybe a0)) arg0) arg1

type (:<=) (NonEmpty a0) arg0 arg1

type (:<=) (NonEmpty a0) arg0 arg1 = Apply (NonEmpty a0) Bool (Apply (NonEmpty a0) (TyFun (NonEmpty a0) Bool -> Type) (TFHelper_1627688021Sym0 (NonEmpty a0)) arg0) arg1

type (:<=) (Either a0 b0) arg0 arg1

type (:<=) (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) Bool (Apply (Either a0 b0) (TyFun (Either a0 b0) Bool -> Type) (TFHelper_1627688021Sym0 (Either a0 b0)) arg0) arg1

type (:<=) (a0, b0) arg0 arg1

type (:<=) (a0, b0) arg0 arg1 = Apply (a0, b0) Bool (Apply (a0, b0) (TyFun (a0, b0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0)) arg0) arg1

type (:<=) (a0, b0, c0) arg0 arg1

type (:<=) (a0, b0, c0) arg0 arg1 = Apply (a0, b0, c0) Bool (Apply (a0, b0, c0) (TyFun (a0, b0, c0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0, c0)) arg0) arg1

type (:<=) (a0, b0, c0, d0) arg0 arg1

type (:<=) (a0, b0, c0, d0) arg0 arg1 = Apply (a0, b0, c0, d0) Bool (Apply (a0, b0, c0, d0) (TyFun (a0, b0, c0, d0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0, c0, d0)) arg0) arg1

type (:<=) (a0, b0, c0, d0, e0) arg0 arg1

type (:<=) (a0, b0, c0, d0, e0) arg0 arg1 = Apply (a0, b0, c0, d0, e0) Bool (Apply (a0, b0, c0, d0, e0) (TyFun (a0, b0, c0, d0, e0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0, c0, d0, e0)) arg0) arg1

type (:<=) (a0, b0, c0, d0, e0, f0) arg0 arg1

type (:<=) (a0, b0, c0, d0, e0, f0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0) Bool (Apply (a0, b0, c0, d0, e0, f0) (TyFun (a0, b0, c0, d0, e0, f0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0, c0, d0, e0, f0)) arg0) arg1

type (:<=) (a0, b0, c0, d0, e0, f0, g0) arg0 arg1

type (:<=) (a0, b0, c0, d0, e0, f0, g0) arg0 arg1 = Apply (a0, b0, c0, d0, e0, f0, g0) Bool (Apply (a0, b0, c0, d0, e0, f0, g0) (TyFun (a0, b0, c0, d0, e0, f0, g0) Bool -> Type) (TFHelper_1627688021Sym0 (a0, b0, c0, d0, e0, f0, g0)) arg0) arg1

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

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) => 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)

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

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 m. PeanoOrder nat => Sing (n :: nat) -> 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 :: (Nat :~: Succ Nat (Zero Nat)) (One Nat)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

zeroOrSucc :: Sing Nat n -> ZeroOrSucc Nat n

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

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

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

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

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

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

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

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

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

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

PeanoOrder Nat

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

leqViewRefl :: Sing Nat n -> LeqView Nat n n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Monomorphicable Nat (Sing Nat)

Associated Types

type MonomorphicRep (Sing Nat) (k1 :: Sing Nat -> *) :: *

Methods

promote :: MonomorphicRep (Sing Nat) k1 -> Monomorphic (Sing Nat) k1

demote :: Monomorphic (Sing Nat) k1 -> MonomorphicRep (Sing Nat) k1