type-natural-0.3.0.0: Type-level natural and proofs of their properties.

Safe HaskellNone
LanguageHaskell98

Data.Type.Natural

Contents

Description

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

Synopsis

Re-exported modules.

Natural Numbers

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

data Nat Source

Constructors

Z 
S Nat 

Instances

Eq Nat Source 
Num Nat Source 
Ord Nat Source 
Show Nat Source 
SingI Nat Z Source 
SingKind Nat (KProxy Nat) Source 
SingI Nat n0 => SingI Nat (S n) Source 
PNum Nat (KProxy Nat) Source 
SNum Nat (KProxy Nat) Source 
POrd Nat (KProxy Nat) Source 
SOrd Nat (KProxy Nat) Source 
SEq Nat (KProxy Nat) Source 
PEq Nat (KProxy Nat) Source 
SDecide Nat (KProxy Nat) Source 
SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$) Source 
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> *) -> *) (:<<=$) Source 
SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 Source 
data Sing Nat where Source 
type FromInteger Nat a0 Source 
type Signum Nat a0 Source 
type Abs Nat a0 Source 
type Negate Nat arg0 = Apply Nat Nat (Negate_1627753616Sym0 Nat) arg0 
type (:*) Nat a0 a1 Source 
type (:-) Nat a0 a1 Source 
type (:+) Nat a0 a1 Source 
type Min Nat a0 a1 Source 
type Max Nat a0 a1 Source 
type (:>=) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641632Sym0 Nat) arg0) arg1 
type (:>) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641599Sym0 Nat) arg0) arg1 
type (:<=) Nat a0 a1 Source 
type (:<) Nat arg0 arg1 = Apply Bool Nat (Apply (TyFun Nat Bool -> *) Nat (TFHelper_1627641533Sym0 Nat) arg0) arg1 
type Compare Nat arg0 arg1 = Apply Ordering Nat (Apply (TyFun Nat Ordering -> *) Nat (Compare_1627641500Sym0 Nat) arg0) arg1 
type (:/=) Nat x y = Not ((:==) Nat x y) 
type (:==) Nat a0 b0 Source 
type Apply Nat Nat SSym0 l0 = SSym1 l0 Source 
type Apply Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0 Source 
type DemoteRep Nat (KProxy Nat) = Nat Source 
type MonomorphicRep Nat (Sing Nat) = Int 
type Apply (TyFun Nat Bool -> *) Nat (:<<=$) l0 = (:<<=$$) l0 Source 

type SSym1 t = S t Source

type ZSym0 = Z Source

Singleton type for Nat.

type SNat = (Sing :: Nat -> *) Source

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where 
data Sing Ordering where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing Nat where 
type MonomorphicRep Nat (Sing Nat) = Int 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

Smart constructors

WARNING: Smart constructors are deprecated as of singletons 0.10, so these are provided only for backward compatibility.

sZ :: SNat Z Source

Deprecated: Smart constructors are no longer needed in singletons; Use SS or SZ instead.

sS :: SNat n -> SNat (S n) Source

Deprecated: Smart constructors are no longer needed in singletons; Use SS or SZ instead.

Arithmetic functions and their singletons.

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

type family Min arg0 arg1 :: a0

Instances

type Min Bool arg0 arg1 = Apply Bool Bool (Apply (TyFun Bool Bool -> *) Bool (Min_1627641698Sym0 Bool) arg0) arg1 
type Min Ordering arg0 arg1 = Apply Ordering Ordering (Apply (TyFun Ordering Ordering -> *) Ordering (Min_1627641698Sym0 Ordering) arg0) arg1 
type Min Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Min_1627641698Sym0 Nat) arg0) arg1 
type Min Symbol arg0 arg1 = Apply Symbol Symbol (Apply (TyFun Symbol Symbol -> *) Symbol (Min_1627641698Sym0 Symbol) arg0) arg1 
type Min () arg0 arg1 = Apply () () (Apply (TyFun () () -> *) () (Min_1627641698Sym0 ()) arg0) arg1 
type Min Nat a0 a1 
type Min [a0] arg0 arg1 = Apply [a0] [a0] (Apply (TyFun [a0] [a0] -> *) [a0] (Min_1627641698Sym0 [a0]) arg0) arg1 
type Min (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (TyFun (Maybe a0) (Maybe a0) -> *) (Maybe a0) (Min_1627641698Sym0 (Maybe a0)) arg0) arg1 
type Min (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (TyFun (Either a0 b0) (Either a0 b0) -> *) (Either a0 b0) (Min_1627641698Sym0 (Either a0 b0)) arg0) arg1 
type Min ((,) a0 b0) arg0 arg1 = Apply ((,) a0 b0) ((,) a0 b0) (Apply (TyFun ((,) a0 b0) ((,) a0 b0) -> *) ((,) a0 b0) (Min_1627641698Sym0 ((,) a0 b0)) arg0) arg1 
type Min ((,,) a0 b0 c0) arg0 arg1 = Apply ((,,) a0 b0 c0) ((,,) a0 b0 c0) (Apply (TyFun ((,,) a0 b0 c0) ((,,) a0 b0 c0) -> *) ((,,) a0 b0 c0) (Min_1627641698Sym0 ((,,) a0 b0 c0)) arg0) arg1 
type Min ((,,,) a0 b0 c0 d0) arg0 arg1 = Apply ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) (Apply (TyFun ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) -> *) ((,,,) a0 b0 c0 d0) (Min_1627641698Sym0 ((,,,) a0 b0 c0 d0)) arg0) arg1 
type Min ((,,,,) a0 b0 c0 d0 e0) arg0 arg1 = Apply ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) (Apply (TyFun ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) -> *) ((,,,,) a0 b0 c0 d0 e0) (Min_1627641698Sym0 ((,,,,) a0 b0 c0 d0 e0)) 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 (TyFun ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) -> *) ((,,,,,) a0 b0 c0 d0 e0 f0) (Min_1627641698Sym0 ((,,,,,) a0 b0 c0 d0 e0 f0)) 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 (TyFun ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) -> *) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Min_1627641698Sym0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0)) arg0) arg1 

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

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

type family Max arg0 arg1 :: a0

Instances

type Max Bool arg0 arg1 = Apply Bool Bool (Apply (TyFun Bool Bool -> *) Bool (Max_1627641665Sym0 Bool) arg0) arg1 
type Max Ordering arg0 arg1 = Apply Ordering Ordering (Apply (TyFun Ordering Ordering -> *) Ordering (Max_1627641665Sym0 Ordering) arg0) arg1 
type Max Nat arg0 arg1 = Apply Nat Nat (Apply (TyFun Nat Nat -> *) Nat (Max_1627641665Sym0 Nat) arg0) arg1 
type Max Symbol arg0 arg1 = Apply Symbol Symbol (Apply (TyFun Symbol Symbol -> *) Symbol (Max_1627641665Sym0 Symbol) arg0) arg1 
type Max () arg0 arg1 = Apply () () (Apply (TyFun () () -> *) () (Max_1627641665Sym0 ()) arg0) arg1 
type Max Nat a0 a1 
type Max [a0] arg0 arg1 = Apply [a0] [a0] (Apply (TyFun [a0] [a0] -> *) [a0] (Max_1627641665Sym0 [a0]) arg0) arg1 
type Max (Maybe a0) arg0 arg1 = Apply (Maybe a0) (Maybe a0) (Apply (TyFun (Maybe a0) (Maybe a0) -> *) (Maybe a0) (Max_1627641665Sym0 (Maybe a0)) arg0) arg1 
type Max (Either a0 b0) arg0 arg1 = Apply (Either a0 b0) (Either a0 b0) (Apply (TyFun (Either a0 b0) (Either a0 b0) -> *) (Either a0 b0) (Max_1627641665Sym0 (Either a0 b0)) arg0) arg1 
type Max ((,) a0 b0) arg0 arg1 = Apply ((,) a0 b0) ((,) a0 b0) (Apply (TyFun ((,) a0 b0) ((,) a0 b0) -> *) ((,) a0 b0) (Max_1627641665Sym0 ((,) a0 b0)) arg0) arg1 
type Max ((,,) a0 b0 c0) arg0 arg1 = Apply ((,,) a0 b0 c0) ((,,) a0 b0 c0) (Apply (TyFun ((,,) a0 b0 c0) ((,,) a0 b0 c0) -> *) ((,,) a0 b0 c0) (Max_1627641665Sym0 ((,,) a0 b0 c0)) arg0) arg1 
type Max ((,,,) a0 b0 c0 d0) arg0 arg1 = Apply ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) (Apply (TyFun ((,,,) a0 b0 c0 d0) ((,,,) a0 b0 c0 d0) -> *) ((,,,) a0 b0 c0 d0) (Max_1627641665Sym0 ((,,,) a0 b0 c0 d0)) arg0) arg1 
type Max ((,,,,) a0 b0 c0 d0 e0) arg0 arg1 = Apply ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) (Apply (TyFun ((,,,,) a0 b0 c0 d0 e0) ((,,,,) a0 b0 c0 d0 e0) -> *) ((,,,,) a0 b0 c0 d0 e0) (Max_1627641665Sym0 ((,,,,) a0 b0 c0 d0 e0)) 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 (TyFun ((,,,,,) a0 b0 c0 d0 e0 f0) ((,,,,,) a0 b0 c0 d0 e0 f0) -> *) ((,,,,,) a0 b0 c0 d0 e0 f0) (Max_1627641665Sym0 ((,,,,,) a0 b0 c0 d0 e0 f0)) 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 (TyFun ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) -> *) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) (Max_1627641665Sym0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0)) arg0) arg1 

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

data MinSym0 l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (MinSym0 k) 
type Apply (TyFun k k -> *) k (MinSym0 k) l0 = MinSym1 k l0 

data MinSym1 l0 l1 :: a0 -> TyFun a0 a0 -> *

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) (MinSym1 k) 
type Apply k k (MinSym1 k l1) l0 = MinSym2 k l1 l0 

type MinSym2 t0 t1 = Min a t0 t1

data MaxSym0 l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) (MaxSym0 k) 
type Apply (TyFun k k -> *) k (MaxSym0 k) l0 = MaxSym1 k l0 

data MaxSym1 l0 l1 :: a0 -> TyFun a0 a0 -> *

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) (MaxSym1 k) 
type Apply k k (MaxSym1 k l1) l0 = MaxSym2 k l1 l0 

type MaxSym2 t0 t1 = Max a t0 t1

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

type family arg0 :+ arg1 :: a0

Instances

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

data (:+$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:+$) k) 
type Apply (TyFun k k -> *) k ((:+$) k) l0 = (:+$$) k l0 

data l0 :+$$ l1 :: a0 -> TyFun a0 a0 -> *

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:+$$) k) 
type Apply k k ((:+$$) k l1) l0 = (:+$$$) k l1 l0 

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

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

Addition for singleton numbers.

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

type family arg0 :* arg1 :: a0

Instances

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

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

Type-level multiplication.

data (:*$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:*$) k) 
type Apply (TyFun k k -> *) k ((:*$) k) l0 = (:*$$) k l0 

data l0 :*$$ l1 :: a0 -> TyFun a0 a0 -> *

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:*$$) k) 
type Apply k k ((:*$$) k l1) l0 = (:*$$$) k l1 l0 

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

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

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

Multiplication for singleton numbers.

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

type family arg0 :- arg1 :: a0

Instances

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

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

Type-level exponentiation.

type family a :** a :: Nat Source

Equations

n :** 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) Source

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

Exponentiation for singleton numbers.

data (:-$) l0 :: TyFun a0 (TyFun a0 a0 -> *) -> *

Instances

SuppressUnusedWarnings (TyFun k (TyFun k k -> *) -> *) ((:-$) k) 
type Apply (TyFun k k -> *) k ((:-$) k) l0 = (:-$$) k l0 

data l0 :-$$ l1 :: a0 -> TyFun a0 a0 -> *

Instances

SuppressUnusedWarnings (k -> TyFun k k -> *) ((:-$$) k) 
type Apply k k ((:-$$) k l1) l0 = (:-$$$) k l1 l0 

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

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

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

Type-level predicate & judgements

data Leq n m where Source

Comparison via GADTs.

Constructors

ZeroLeq :: SNat m -> Leq Zero m 
SuccLeqSucc :: Leq n m -> Leq (S n) (S m) 

class n :<= m Source

Comparison via type-class.

Instances

Z :<= n Source 
(:<=) n m => (S n) :<= (S m) Source 

type family a :<<= a :: Bool Source

Boolean-valued type-level comparison function.

Equations

Z :<<= _z_1627454690 = TrueSym0 
(S _z_1627454693) :<<= Z = FalseSym0 
(S n) :<<= (S m) = Apply (Apply (:<<=$) n) m 

type (:<<=$$$) t t = (:<<=) t t Source

(%:<<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<<=$) t) t :: Bool) Source

type LeqInstance n m = Dict (n :<= m) Source

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

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

type LeqTrueInstance a b = Dict ((a :<<= b) ~ True) Source

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

Conversion functions

natToInt :: Integral n => Nat -> n Source

Convert Nat into normal integers.

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

Convert integral numbers into Nat

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

Convert 'SNat n' into normal integers.

Quasi quotes for natural numbers

nat :: QuasiQuoter Source

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

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

snat :: QuasiQuoter Source

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

For example: [snat|12|] %+ [snat| 5 |], sing :: [snat| 12 |], f [snat| 12 |] = "hey"

Properties of natural numbers

succCongEq :: (n :=: m) -> S n :=: S m Source

plusCongR :: SNat n -> (m :=: m') -> (m :+ n) :=: (m' :+ n) Source

plusCongL :: SNat n -> (m :=: m') -> (n :+ m) :=: (n :+ m') Source

succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m) Source

succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m) Source

plusZR :: SNat n -> (n :+: Z) :=: n Source

plusZL :: SNat n -> (Z :+: n) :=: n Source

eqPreservesS :: (n :=: m) -> S n :=: S m Source

plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l) Source

multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l) Source

multComm :: SNat n -> SNat m -> (n :* m) :=: (m :* n) Source

multOneL :: SNat n -> (One :* n) :=: n Source

multOneR :: SNat n -> (n :* One) :=: n Source

snEqZAbsurd :: (S n :=: Z) -> a Source

succInjective :: (S n :=: S m) -> n :=: m Source

plusInjectiveL :: SNat n -> SNat m -> SNat l -> ((n :+ m) :=: (n :+ l)) -> m :=: l Source

plusInjectiveR :: SNat n -> SNat m -> SNat l -> ((n :+ l) :=: (m :+ l)) -> n :=: m Source

plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l)) Source

multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l)) Source

multCongL :: SNat n -> (m :=: l) -> (n :* m) :=: (n :* l) Source

multCongR :: SNat n -> (m :=: l) -> (m :* n) :=: (l :* n) Source

plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n) Source

minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l) Source

eqSuccMinus :: ((m :<<= n) ~ True) => SNat n -> SNat m -> (S n :-: m) :=: S (n :-: m) Source

plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n Source

plusMinusEqR :: SNat n -> SNat m -> ((m :+: n) :-: m) :=: n Source

plusSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m) Source

plusNeutralR :: SNat n -> SNat m -> ((n :+ m) :=: n) -> m :=: Z Source

plusNeutralL :: SNat n -> SNat m -> ((n :+ m) :=: m) -> n :=: Z Source

leqRhs :: Leq n m -> SNat m Source

leqLhs :: Leq n m -> SNat n Source

minComm :: SNat n -> SNat m -> Min n m :=: Min m n Source

maxZL :: SNat n -> Max Z n :=: n Source

maxComm :: SNat n -> SNat m -> Max n m :=: Max m n Source

maxZR :: SNat n -> Max n Z :=: n Source

Properties of ordering Leq

leqRefl :: SNat n -> Leq n n Source

leqSucc :: SNat n -> Leq n (S n) Source

leqTrans :: Leq n m -> Leq m l -> Leq n l Source

plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k) Source

plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m) Source

plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m) Source

minLeqL :: SNat n -> SNat m -> Leq (Min n m) n Source

minLeqR :: SNat n -> SNat m -> Leq (Min n m) m Source

leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m Source

maxLeqL :: SNat n -> SNat m -> Leq n (Max n m) Source

maxLeqR :: SNat n -> SNat m -> Leq m (Max n m) Source

leqSnZAbsurd :: Leq (S n) Z -> a Source

leqSnLeq :: Leq (S n) m -> Leq n m Source

leqPred :: Leq (S n) (S m) -> Leq n m Source

leqSnnAbsurd :: Leq (S n) n -> a Source

Useful type synonyms and constructors

type family Zero :: Nat Source

Equations

Zero = ZSym0 

type family One :: Nat Source

Equations

One = Apply SSym0 ZeroSym0 

type family Two :: Nat Source

Equations

Two = Apply SSym0 OneSym0 

type family Three :: Nat Source

Equations

Three = Apply SSym0 TwoSym0 

type family Four :: Nat Source

Equations

Four = Apply SSym0 ThreeSym0 

type family Five :: Nat Source

Equations

Five = Apply SSym0 FourSym0 

type family Six :: Nat Source

Equations

Six = Apply SSym0 FiveSym0 

type family Seven :: Nat Source

Equations

Seven = Apply SSym0 SixSym0 

type family Eight :: Nat Source

Equations

Eight = Apply SSym0 SevenSym0 

type family Nine :: Nat Source

Equations

Nine = Apply SSym0 EightSym0 

type family Ten :: Nat Source

Equations

Ten = Apply SSym0 NineSym0 

type family Eleven :: Nat Source

Equations

Eleven = Apply SSym0 TenSym0 

type family Twelve :: Nat Source

type family Thirteen :: Nat Source

type family Fourteen :: Nat Source

type family Fifteen :: Nat Source

type family Sixteen :: Nat Source

type family Seventeen :: Nat Source

type family Eighteen :: Nat Source

type family Nineteen :: Nat Source

type family Twenty :: Nat Source

type family N0 :: Nat Source

Equations

N0 = ZeroSym0 

type family N1 :: Nat Source

Equations

N1 = OneSym0 

type family N2 :: Nat Source

Equations

N2 = TwoSym0 

type family N3 :: Nat Source

Equations

N3 = ThreeSym0 

type family N4 :: Nat Source

Equations

N4 = FourSym0 

type family N5 :: Nat Source

Equations

N5 = FiveSym0 

type family N6 :: Nat Source

Equations

N6 = SixSym0 

type family N7 :: Nat Source

Equations

N7 = SevenSym0 

type family N8 :: Nat Source

Equations

N8 = EightSym0 

type family N9 :: Nat Source

Equations

N9 = NineSym0 

type family N10 :: Nat Source

Equations

N10 = TenSym0 

type family N11 :: Nat Source

Equations

N11 = ElevenSym0 

type family N12 :: Nat Source

Equations

N12 = TwelveSym0 

type family N13 :: Nat Source

Equations

N13 = ThirteenSym0 

type family N14 :: Nat Source

Equations

N14 = FourteenSym0 

type family N15 :: Nat Source

Equations

N15 = FifteenSym0 

type family N16 :: Nat Source

Equations

N16 = SixteenSym0 

type family N17 :: Nat Source

Equations

N17 = SeventeenSym0 

type family N18 :: Nat Source

Equations

N18 = EighteenSym0 

type family N19 :: Nat Source

Equations

N19 = NineteenSym0 

type family N20 :: Nat Source

Equations

N20 = TwentySym0