Safe Haskell	Safe
Language	Haskell98

Data.Repa.Scalar.Singleton.Nat

Contents

Description

Singleton-typed natural numbers and arithmetic.

Used for indexing into hetrogenous list types.

Synopsis

data N
- = Z
- | S N
data Nat (n :: N) where
- Zero :: Nat Z
- Succ :: Nat n -> Nat (S n)
class Add x y where
- type AddR x y :: N
- add :: Nat x -> Nat y -> Nat (AddR x y)
class Mul x y where
- type MulR x y :: N
- mul :: Nat x -> Nat y -> Nat (MulR x y)
nat0 :: Nat Z
nat1 :: Nat (S Z)
nat2 :: Nat (S (S Z))
nat3 :: Nat (S (S (S Z)))
nat4 :: Nat (S (S (S (S Z))))
nat5 :: Nat (S (S (S (S (S Z)))))
nat6 :: Nat (S (S (S (S (S (S Z))))))
nat7 :: Nat (S (S (S (S (S (S (S Z)))))))
nat8 :: Nat (S (S (S (S (S (S (S (S Z))))))))
nat9 :: Nat (S (S (S (S (S (S (S (S (S Z)))))))))

Documentation

Peano natural numbers.

Constructors

Z
S N

Instances

Show N Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Methods showsPrec :: Int -> N -> ShowS # show :: N -> String # showList :: [N] -> ShowS #

data Nat (n :: N) where Source #

Peano natural number singletons.

Constructors

Zero :: Nat Z
Succ :: Nat n -> Nat (S n)

Instances

Show (Nat n) Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Methods showsPrec :: Int -> Nat n -> ShowS # show :: Nat n -> String # showList :: [Nat n] -> ShowS #

class Add x y where Source #

Associated Types

type AddR x y :: N Source #

Methods

add :: Nat x -> Nat y -> Nat (AddR x y) Source #

Addition of singleton typed natural numbers.

Instances

Add Z x Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Associated Types type AddR Z x :: N Source # Methods add :: Nat Z -> Nat x -> Nat (AddR Z x) Source #
Add x (S y) => Add (S x) y Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Associated Types type AddR (S x) y :: N Source # Methods add :: Nat (S x) -> Nat y -> Nat (AddR (S x) y) Source #

class Mul x y where Source #

Associated Types

type MulR x y :: N Source #

Methods

mul :: Nat x -> Nat y -> Nat (MulR x y) Source #

Multiplication of singleton typed natural numbers.

Instances

Mul Z x Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Associated Types type MulR Z x :: N Source # Methods mul :: Nat Z -> Nat x -> Nat (MulR Z x) Source #
(Mul x y, Add (MulR x y) y) => Mul (S x) y Source #
Instance details Defined in Data.Repa.Scalar.Singleton.Nat Associated Types type MulR (S x) y :: N Source # Methods mul :: Nat (S x) -> Nat y -> Nat (MulR (S x) y) Source #

Literals

nat5 :: Nat (S (S (S (S (S Z))))) Source #

nat6 :: Nat (S (S (S (S (S (S Z)))))) Source #

nat7 :: Nat (S (S (S (S (S (S (S Z))))))) Source #

nat8 :: Nat (S (S (S (S (S (S (S (S Z)))))))) Source #

nat9 :: Nat (S (S (S (S (S (S (S (S (S Z))))))))) Source #