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

Eq Nat

Num Nat

Ord Nat

Show Nat

SingI Nat Z

SingKind Nat (KProxy Nat)

SingI Nat n0 => SingI Nat (S n)

PNum Nat (KProxy Nat)

SNum Nat (KProxy Nat)

POrd Nat (KProxy Nat)

SOrd Nat (KProxy Nat)

SEq Nat (KProxy Nat)

PEq Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> *) -> *) (:<<=$)

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

data Sing Nat where

• SZ :: (~) Nat z Z => Sing Nat z
• SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z

type FromInteger Nat a0

type Signum Nat a0

type Abs Nat a0

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

type (:*) Nat a0 a1

type (:-) Nat a0 a1

type (:+) Nat a0 a1

type Min Nat a0 a1

type Max Nat a0 a1

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

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

type Apply Nat Nat SSym0 l0 = SSym1 l0

type Apply Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0

type DemoteRep Nat (KProxy Nat) = Nat

type MonomorphicRep Nat (Sing Nat) = Int

type Apply (TyFun Nat Bool -> *) Nat (:<<=$) l0 = (:<<=$$) l0

data SSym0 l

Instances

SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0

type Apply Nat Nat SSym0 l0 = SSym1 l0

type SSym1 t = S t

type ZSym0 = Z

Singleton type for Nat.

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

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where

• SFalse :: (~) Bool z0 False => Sing Bool z0
• STrue :: (~) Bool z0 True => Sing Bool z0

data Sing Ordering where

• SLT :: (~) Ordering z0 LT => Sing Ordering z0
• SEQ :: (~) Ordering z0 EQ => Sing Ordering z0
• SGT :: (~) Ordering z0 GT => Sing Ordering z0

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

data Sing () where

• STuple0 :: (~) () z0 () => Sing () z0

data Sing Nat where

• SZ :: (~) Nat z Z => Sing Nat z
• SS :: (~) Nat z (S n) => Sing Nat n -> Sing Nat z

type MonomorphicRep Nat (Sing Nat) = Int

data Sing [a0] where

• SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0
• SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0

data Sing (Maybe a0) where

• SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0
• SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0

data Sing (TyFun k1 k2 -> *) = SLambda {

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

}

data Sing (Either a0 b0) where

• SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0
• SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0

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

• STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0

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

• STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0

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

• STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0

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

• STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0

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

• STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

Smart constructors

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

sZ :: SNat Z

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

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

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

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

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

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

Multiplication for singleton numbers.

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

type family arg0 :- arg1 :: a0

Instances

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

type (:-) Nat a0 a1

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

Type-level exponentiation.

type family a :** a :: Nat

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)

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

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

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)

class n :<= m

Comparison via type-class.

Instances

Z :<= n

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

type family a :<<= a :: Bool

Boolean-valued type-level comparison function.

Equations

Z :<<= _z_1627454690 = TrueSym0

(S _z_1627454693) :<<= Z = FalseSym0

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

data (:<<=$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Bool -> *) -> *) (:<<=$)

type Apply (TyFun Nat Bool -> *) Nat (:<<=$) l0 = (:<<=$$) l0

data l :<<=$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Bool -> *) (:<<=$$)

type Apply Bool Nat ((:<<=$$) l1) l0 = (:<<=$$$) l1 l0

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

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

type LeqInstance n m = Dict (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

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

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

Conversion functions

natToInt :: Integral n => Nat -> n

Convert Nat into normal integers.

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

Convert integral numbers into Nat

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

Convert 'SNat n' into normal integers.

Quasi quotes for natural numbers

nat :: QuasiQuoter

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

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

snat :: QuasiQuoter

Quotesi-quoter for SNat. This can be used for an expression, 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

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

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

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

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

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

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

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

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

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

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

multZL :: SNat m -> (Zero :* m) :=: Zero

multZR :: SNat m -> (m :* Zero) :=: Zero

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

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

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

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

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

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

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

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

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

sAndPlusOne :: SNat n -> S n :=: (n :+: One)

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

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

minusNilpotent :: SNat n -> (n :-: n) :=: Zero

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

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

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

zAbsorbsMinR :: SNat n -> Min n Z :=: Z

zAbsorbsMinL :: SNat n -> Min Z n :=: Z

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

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

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

leqRhs :: Leq n m -> SNat m

leqLhs :: Leq n m -> SNat n

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

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

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

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

Properties of ordering Leq

leqRefl :: SNat n -> Leq n n

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

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

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

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

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

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

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

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

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

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

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

leqnZElim :: Leq n Z -> n :=: Z

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

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

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

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

Equations

Zero = ZSym0

type family One :: Nat

Equations

One = Apply SSym0 ZeroSym0

type family Two :: Nat

Equations

Two = Apply SSym0 OneSym0

type family Three :: Nat

Equations

Three = Apply SSym0 TwoSym0

type family Four :: Nat

Equations

Four = Apply SSym0 ThreeSym0

type family Five :: Nat

Equations

Five = Apply SSym0 FourSym0

type family Six :: Nat

Equations

Six = Apply SSym0 FiveSym0

type family Seven :: Nat

Equations

Seven = Apply SSym0 SixSym0

type family Eight :: Nat

Equations

Eight = Apply SSym0 SevenSym0

type family Nine :: Nat

Equations

Nine = Apply SSym0 EightSym0

type family Ten :: Nat

Equations

Ten = Apply SSym0 NineSym0

type family Eleven :: Nat

Equations

Eleven = Apply SSym0 TenSym0

type family Twelve :: Nat

Equations

Twelve = Apply SSym0 ElevenSym0

type family Thirteen :: Nat

Equations

Thirteen = Apply SSym0 TwelveSym0

type family Fourteen :: Nat

Equations

Fourteen = Apply SSym0 ThirteenSym0

type family Fifteen :: Nat

Equations

Fifteen = Apply SSym0 FourteenSym0

type family Sixteen :: Nat

Equations

Sixteen = Apply SSym0 FifteenSym0

type family Seventeen :: Nat

Equations

Seventeen = Apply SSym0 SixteenSym0

type family Eighteen :: Nat

Equations

Eighteen = Apply SSym0 SeventeenSym0

type family Nineteen :: Nat

Equations

Nineteen = Apply SSym0 EighteenSym0

type family Twenty :: Nat

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

Equations

N0 = ZeroSym0

type family N1 :: Nat

Equations

N1 = OneSym0

type family N2 :: Nat

Equations

N2 = TwoSym0

type family N3 :: Nat

Equations

N3 = ThreeSym0

type family N4 :: Nat

Equations

N4 = FourSym0

type family N5 :: Nat

Equations

N5 = FiveSym0

type family N6 :: Nat

Equations

N6 = SixSym0

type family N7 :: Nat

Equations

N7 = SevenSym0

type family N8 :: Nat

Equations

N8 = EightSym0

type family N9 :: Nat

Equations

N9 = NineSym0

type family N10 :: Nat

Equations

N10 = TenSym0

type family N11 :: Nat

Equations

N11 = ElevenSym0

type family N12 :: Nat

Equations

N12 = TwelveSym0

type family N13 :: Nat

Equations

N13 = ThirteenSym0

type family N14 :: Nat

Equations

N14 = FourteenSym0

type family N15 :: Nat

Equations

N15 = FifteenSym0

type family N16 :: Nat

Equations

N16 = SixteenSym0

type family N17 :: Nat

Equations

N17 = SeventeenSym0

type family N18 :: Nat

Equations

N18 = EighteenSym0

type family N19 :: Nat

Equations

N19 = NineteenSym0

type family N20 :: Nat

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)