Numerical.Nat

Documentation

data Nat

Constructors

S !Nat

Z

Instances

Eq Nat

Defined in Numerical.Nat

Methods

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

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

Data Nat

Defined in Numerical.Nat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Nat -> c Nat

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Nat

toConstr :: Nat -> Constr

dataTypeOf :: Nat -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Nat)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)

gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r

gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Nat -> m Nat

Read Nat

Defined in Numerical.Nat

Methods

readsPrec :: Int -> ReadS Nat

readList :: ReadS [Nat]

readPrec :: ReadPrec Nat

readListPrec :: ReadPrec [Nat]

Show Nat

Defined in Numerical.Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

type N0 = Z

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9

data SNat :: Nat -> * where

Constructors

SZero :: SNat Z

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

type family n1 + n2 where ...

Equations

Z + n2 = n2

(S n1') + n2 = S (n1' + n2)

plus_id_r :: SNat n -> (n + Z) :~: n

plus_succ_r :: SNat n1 -> Proxy n2 -> (n1 + S n2) :~: S (n1 + n2)

gcastWith :: (a :~: b) -> ((a ~ b) -> r) -> r

Generalized form of type-safe cast using propositional equality

data Proxy (t :: k) :: forall k. k -> Type

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy

>>> Proxy :: Proxy Functor
Proxy

>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy

Instances

Generic1 (Proxy :: k -> Type)

Defined in GHC.Generics

Associated Types

type Rep1 Proxy :: k -> Type

Methods

from1 :: Proxy a -> Rep1 Proxy a

to1 :: Rep1 Proxy a -> Proxy a

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(>>=) :: Proxy a -> (a -> Proxy b) -> Proxy b

(>>) :: Proxy a -> Proxy b -> Proxy b

return :: a -> Proxy a

fail :: String -> Proxy a

Functor (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

fmap :: (a -> b) -> Proxy a -> Proxy b

(<$) :: a -> Proxy b -> Proxy a

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

pure :: a -> Proxy a

(<*>) :: Proxy (a -> b) -> Proxy a -> Proxy b

liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c

(*>) :: Proxy a -> Proxy b -> Proxy b

(<*) :: Proxy a -> Proxy b -> Proxy a

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Foldable

Methods

fold :: Monoid m => Proxy m -> m

foldMap :: Monoid m => (a -> m) -> Proxy a -> m

foldr :: (a -> b -> b) -> b -> Proxy a -> b

foldr' :: (a -> b -> b) -> b -> Proxy a -> b

foldl :: (b -> a -> b) -> b -> Proxy a -> b

foldl' :: (b -> a -> b) -> b -> Proxy a -> b

foldr1 :: (a -> a -> a) -> Proxy a -> a

foldl1 :: (a -> a -> a) -> Proxy a -> a

toList :: Proxy a -> [a]

null :: Proxy a -> Bool

length :: Proxy a -> Int

elem :: Eq a => a -> Proxy a -> Bool

maximum :: Ord a => Proxy a -> a

minimum :: Ord a => Proxy a -> a

sum :: Num a => Proxy a -> a

product :: Num a => Proxy a -> a

Traversable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Defined in Data.Traversable

Methods

traverse :: Applicative f => (a -> f b) -> Proxy a -> f (Proxy b)

sequenceA :: Applicative f => Proxy (f a) -> f (Proxy a)

mapM :: Monad m => (a -> m b) -> Proxy a -> m (Proxy b)

sequence :: Monad m => Proxy (m a) -> m (Proxy a)

Eq1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftEq :: (a -> b -> Bool) -> Proxy a -> Proxy b -> Bool

Ord1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftCompare :: (a -> b -> Ordering) -> Proxy a -> Proxy b -> Ordering

Read1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Proxy a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Proxy a]

Show1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Functor.Classes

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy a] -> ShowS

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

empty :: Proxy a

(<|>) :: Proxy a -> Proxy a -> Proxy a

some :: Proxy a -> Proxy [a]

many :: Proxy a -> Proxy [a]

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

mzero :: Proxy a

mplus :: Proxy a -> Proxy a -> Proxy a

Bounded (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

minBound :: Proxy t

maxBound :: Proxy t

Enum (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s

pred :: Proxy s -> Proxy s

toEnum :: Int -> Proxy s

fromEnum :: Proxy s -> Int

enumFrom :: Proxy s -> [Proxy s]

enumFromThen :: Proxy s -> Proxy s -> [Proxy s]

enumFromTo :: Proxy s -> Proxy s -> [Proxy s]

enumFromThenTo :: Proxy s -> Proxy s -> Proxy s -> [Proxy s]

Eq (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

(==) :: Proxy s -> Proxy s -> Bool

(/=) :: Proxy s -> Proxy s -> Bool

Data t => Data (Proxy t)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Proxy t -> c (Proxy t)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Proxy t)

toConstr :: Proxy t -> Constr

dataTypeOf :: Proxy t -> DataType

dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (Proxy t))

dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (Proxy t))

gmapT :: (forall b. Data b => b -> b) -> Proxy t -> Proxy t

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Proxy t -> r

gmapQ :: (forall d. Data d => d -> u) -> Proxy t -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Proxy t -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Proxy t -> m (Proxy t)

Ord (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering

(<) :: Proxy s -> Proxy s -> Bool

(<=) :: Proxy s -> Proxy s -> Bool

(>) :: Proxy s -> Proxy s -> Bool

(>=) :: Proxy s -> Proxy s -> Bool

max :: Proxy s -> Proxy s -> Proxy s

min :: Proxy s -> Proxy s -> Proxy s

Read (Proxy t)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

readsPrec :: Int -> ReadS (Proxy t)

readList :: ReadS [Proxy t]

readPrec :: ReadPrec (Proxy t)

readListPrec :: ReadPrec [Proxy t]

Show (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

showsPrec :: Int -> Proxy s -> ShowS

show :: Proxy s -> String

showList :: [Proxy s] -> ShowS

Ix (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

range :: (Proxy s, Proxy s) -> [Proxy s]

index :: (Proxy s, Proxy s) -> Proxy s -> Int

unsafeIndex :: (Proxy s, Proxy s) -> Proxy s -> Int

inRange :: (Proxy s, Proxy s) -> Proxy s -> Bool

rangeSize :: (Proxy s, Proxy s) -> Int

unsafeRangeSize :: (Proxy s, Proxy s) -> Int

Generic (Proxy t)

Defined in GHC.Generics

Associated Types

type Rep (Proxy t) :: Type -> Type

Methods

from :: Proxy t -> Rep (Proxy t) x

to :: Rep (Proxy t) x -> Proxy t

Semigroup (Proxy s)

Since: base-4.9.0.0

Defined in Data.Proxy

Methods

(<>) :: Proxy s -> Proxy s -> Proxy s

sconcat :: NonEmpty (Proxy s) -> Proxy s

stimes :: Integral b => b -> Proxy s -> Proxy s

Monoid (Proxy s)

Since: base-4.7.0.0

Defined in Data.Proxy

Methods

mempty :: Proxy s

mappend :: Proxy s -> Proxy s -> Proxy s

mconcat :: [Proxy s] -> Proxy s

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep1 (Proxy :: k -> Type) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> Type))

type Rep (Proxy t)

Since: base-4.6.0.0

Defined in GHC.Generics

type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: Type -> Type))

type LitNat = Nat

type family U (n :: Nat) :: Nat where ...

Equations

U 0 = Z

U n = S (U ((-) n 1))