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 Demote Nat = (r :: *)

Methods

fromSing :: Sing Nat a -> Demote Nat

toSing :: Demote Nat -> SomeSing Nat

PEnum Nat

Associated Types

type Succ Nat (arg :: Nat) :: a

type Pred Nat (arg :: Nat) :: a

type ToEnum Nat (arg :: Nat) :: a

type FromEnum Nat (arg :: Nat) :: Nat

type EnumFromTo Nat (arg :: Nat) (arg1 :: Nat) :: [a]

type EnumFromThenTo Nat (arg :: Nat) (arg1 :: Nat) (arg2 :: Nat) :: [a]

SEnum Nat

Methods

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

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

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

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

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

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

PNum Nat

Associated Types

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

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

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

type Negate Nat (arg :: Nat) :: a

type Abs Nat (arg :: Nat) :: a

type Signum Nat (arg :: Nat) :: a

type FromInteger Nat (arg :: Nat) :: a

SNum Nat

Methods

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

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

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

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

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

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

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

POrd Nat

Associated Types

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

type (Nat :< (arg :: Nat)) (arg1 :: Nat) :: Bool

type (Nat :<= (arg :: Nat)) (arg1 :: Nat) :: Bool

type (Nat :> (arg :: Nat)) (arg1 :: Nat) :: Bool

type (Nat :>= (arg :: Nat)) (arg1 :: Nat) :: Bool

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

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

SOrd Nat

Methods

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

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

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

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

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

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

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

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)

PEq Nat

Associated Types

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

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

SDecide Nat

Methods

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

SingI Nat Z

Methods

sing :: Sing Z a

SingI Nat n => SingI Nat (S n)

Methods

sing :: Sing (S n) a

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 Demote Nat

type Demote Nat = Nat

data Sing Nat

data Sing Nat where

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

type FromEnum Nat a

type FromEnum Nat a

type ToEnum Nat a

type ToEnum Nat a

type Pred Nat a

type Pred Nat a

type Succ Nat a

type Succ Nat a

type FromInteger Nat a

type FromInteger Nat a

type Signum Nat a

type Signum Nat a

type Abs Nat a

type Abs Nat a

type Negate Nat arg

type Negate Nat arg = Apply Nat Nat (Negate_6989586621679400878Sym0 Nat) arg

type EnumFromTo Nat arg arg1

type EnumFromTo Nat arg arg1 = Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromTo_6989586621679800012Sym0 Nat) arg) arg1

type (:*) Nat a1 a2

type (:*) Nat a1 a2

type (:-) Nat a1 a2

type (:-) Nat a1 a2

type (:+) Nat a1 a2

type (:+) Nat a1 a2

type Min Nat a1 a2

type Min Nat a1 a2

type Max Nat a1 a2

type Max Nat a1 a2

type (:>=) Nat a1 a2

type (:>=) Nat a1 a2

type (:>) Nat a1 a2

type (:>) Nat a1 a2

type (:<=) Nat a1 a2

type (:<=) Nat a1 a2

type (:<) Nat a1 a2

type (:<) Nat a1 a2

type Compare Nat arg arg1

type Compare Nat arg arg1 = Apply Nat Ordering (Apply Nat (TyFun Nat Ordering -> Type) (Compare_6989586621679304250Sym0 Nat) arg) arg1

type (:/=) Nat x y

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

type (:==) Nat a b

type (:==) Nat a b

type Apply Nat Nat SSym0 l

type Apply Nat Nat SSym0 l = S l

type EnumFromThenTo Nat arg arg1 arg2

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

data SSym0 (l :: TyFun Nat Nat)

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply Nat Nat SSym0 l

type Apply Nat Nat SSym0 l = S l

type SSym1 (t :: Nat) = 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 z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

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 () z

data Sing Nat

data Sing Nat where

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

data Sing [a]

data Sing [a] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a)

data Sing (Maybe a) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a)

data Sing (NonEmpty a) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a b)

data Sing (Either a b) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a, b)

data Sing (a, b) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

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

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

}

data Sing (a, b, c)

data Sing (a, b, c) where

• STuple3 :: Sing (a, b, c) z

data Sing (a, b, c, d)

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

• STuple4 :: Sing (a, b, c, d) z

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

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

• STuple5 :: Sing (a, b, c, d, e) z

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

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

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

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

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

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

Arithmetic functions and their singletons.

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

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

Instances

type Min Bool arg1 arg2

type Min Bool arg1 arg2 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Min_6989586621679304448Sym0 Bool) arg1) arg2

type Min Ordering arg1 arg2

type Min Ordering arg1 arg2 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Min_6989586621679304448Sym0 Ordering) arg1) arg2

type Min Nat arg1 arg2

type Min Nat arg1 arg2 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Min_6989586621679304448Sym0 Nat) arg1) arg2

type Min Symbol arg1 arg2

type Min Symbol arg1 arg2 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Min_6989586621679304448Sym0 Symbol) arg1) arg2

type Min () arg1 arg2

type Min () arg1 arg2 = Apply () () (Apply () (TyFun () () -> Type) (Min_6989586621679304448Sym0 ()) arg1) arg2

type Min Nat a1 a2

type Min Nat a1 a2

type Min [a] arg1 arg2

type Min [a] arg1 arg2 = Apply [a] [a] (Apply [a] (TyFun [a] [a] -> Type) (Min_6989586621679304448Sym0 [a]) arg1) arg2

type Min (Maybe a) arg1 arg2

type Min (Maybe a) arg1 arg2 = Apply (Maybe a) (Maybe a) (Apply (Maybe a) (TyFun (Maybe a) (Maybe a) -> Type) (Min_6989586621679304448Sym0 (Maybe a)) arg1) arg2

type Min (NonEmpty a) arg1 arg2

type Min (NonEmpty a) arg1 arg2 = Apply (NonEmpty a) (NonEmpty a) (Apply (NonEmpty a) (TyFun (NonEmpty a) (NonEmpty a) -> Type) (Min_6989586621679304448Sym0 (NonEmpty a)) arg1) arg2

type Min (Either a b) arg1 arg2

type Min (Either a b) arg1 arg2 = Apply (Either a b) (Either a b) (Apply (Either a b) (TyFun (Either a b) (Either a b) -> Type) (Min_6989586621679304448Sym0 (Either a b)) arg1) arg2

type Min (a, b) arg1 arg2

type Min (a, b) arg1 arg2 = Apply (a, b) (a, b) (Apply (a, b) (TyFun (a, b) (a, b) -> Type) (Min_6989586621679304448Sym0 (a, b)) arg1) arg2

type Min (a, b, c) arg1 arg2

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

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

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

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

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

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

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

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

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

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

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

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

Instances

type Max Bool arg1 arg2

type Max Bool arg1 arg2 = Apply Bool Bool (Apply Bool (TyFun Bool Bool -> Type) (Max_6989586621679304415Sym0 Bool) arg1) arg2

type Max Ordering arg1 arg2

type Max Ordering arg1 arg2 = Apply Ordering Ordering (Apply Ordering (TyFun Ordering Ordering -> Type) (Max_6989586621679304415Sym0 Ordering) arg1) arg2

type Max Nat arg1 arg2

type Max Nat arg1 arg2 = Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) (Max_6989586621679304415Sym0 Nat) arg1) arg2

type Max Symbol arg1 arg2

type Max Symbol arg1 arg2 = Apply Symbol Symbol (Apply Symbol (TyFun Symbol Symbol -> Type) (Max_6989586621679304415Sym0 Symbol) arg1) arg2

type Max () arg1 arg2

type Max () arg1 arg2 = Apply () () (Apply () (TyFun () () -> Type) (Max_6989586621679304415Sym0 ()) arg1) arg2

type Max Nat a1 a2

type Max Nat a1 a2

type Max [a] arg1 arg2

type Max [a] arg1 arg2 = Apply [a] [a] (Apply [a] (TyFun [a] [a] -> Type) (Max_6989586621679304415Sym0 [a]) arg1) arg2

type Max (Maybe a) arg1 arg2

type Max (Maybe a) arg1 arg2 = Apply (Maybe a) (Maybe a) (Apply (Maybe a) (TyFun (Maybe a) (Maybe a) -> Type) (Max_6989586621679304415Sym0 (Maybe a)) arg1) arg2

type Max (NonEmpty a) arg1 arg2

type Max (NonEmpty a) arg1 arg2 = Apply (NonEmpty a) (NonEmpty a) (Apply (NonEmpty a) (TyFun (NonEmpty a) (NonEmpty a) -> Type) (Max_6989586621679304415Sym0 (NonEmpty a)) arg1) arg2

type Max (Either a b) arg1 arg2

type Max (Either a b) arg1 arg2 = Apply (Either a b) (Either a b) (Apply (Either a b) (TyFun (Either a b) (Either a b) -> Type) (Max_6989586621679304415Sym0 (Either a b)) arg1) arg2

type Max (a, b) arg1 arg2

type Max (a, b) arg1 arg2 = Apply (a, b) (a, b) (Apply (a, b) (TyFun (a, b) (a, b) -> Type) (Max_6989586621679304415Sym0 (a, b)) arg1) arg2

type Max (a, b, c) arg1 arg2

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

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

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

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

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

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

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

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

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

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

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

Instances

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

Methods

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

type Apply a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type) (MinSym0 a6989586621679302787) l

type Apply a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type) (MinSym0 a6989586621679302787) l = MinSym1 a6989586621679302787 l

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

Instances

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

Methods

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

type Apply a a (MinSym1 a l1) l2

type Apply a a (MinSym1 a l1) l2 = Min a l1 l2

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

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

Instances

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

Methods

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

type Apply a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type) (MaxSym0 a6989586621679302787) l

type Apply a6989586621679302787 (TyFun a6989586621679302787 a6989586621679302787 -> Type) (MaxSym0 a6989586621679302787) l = MaxSym1 a6989586621679302787 l

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

Instances

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

Methods

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

type Apply a a (MaxSym1 a l1) l2

type Apply a a (MaxSym1 a l1) l2 = Max a l1 l2

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

type (+) a b = (:+) a b infixl 6

type (+@#@$) = (:+$)

type (+@#@$$) = (:+$$)

type (+@#@$$$) a b = (:+$$$) a b

(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6

type * a b = (:*) a b infixl 7

type (*@#@$) = (:*$)

type (*@#@$$) = (:*$$)

type (*@#@$$$) a b = (:*$$$) a b

(%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b) infixl 7

type (-) a b = (:-) a b infixl 6

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

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

type (-@#@$) = (:-$)

type (-@#@$$) = (:-$$)

type (-@#@$$$) a b = (:-$$$) a b

(%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b) 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 (<=) a b = (:<=) a b infix 4

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, 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

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

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 :: Nat). 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

toNatural :: Sing Nat n -> Natural

fromNatural :: Natural -> SomeSing Nat

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