Data.Repa.Scalar.Singleton.Nat

Singleton-typed natural numbers and arithmetic.

Used for indexing into hetrogenous list types.

Documentation

data N

Peano natural numbers.

Constructors

Z

S N

Instances

Show N

Defined in Data.Repa.Scalar.Singleton.Nat

Methods

showsPrec :: Int -> N -> ShowS

show :: N -> String

showList :: [N] -> ShowS

data Nat (n :: N) where

Peano natural number singletons.

Constructors

Zero :: Nat Z

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

Instances

Show (Nat n)

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

Associated Types

type AddR x y :: N

Methods

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

Addition of singleton typed natural numbers.

Instances

Add Z x

Defined in Data.Repa.Scalar.Singleton.Nat

Associated Types

type AddR Z x :: N

Methods

add :: Nat Z -> Nat x -> Nat (AddR Z x)

Add x (S y) => Add (S x) y

Defined in Data.Repa.Scalar.Singleton.Nat

Associated Types

type AddR (S x) y :: N

Methods

add :: Nat (S x) -> Nat y -> Nat (AddR (S x) y)

class Mul x y where

Associated Types

type MulR x y :: N

Methods

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

Multiplication of singleton typed natural numbers.

Instances

Mul Z x

Defined in Data.Repa.Scalar.Singleton.Nat

Associated Types

type MulR Z x :: N

Methods

mul :: Nat Z -> Nat x -> Nat (MulR Z x)

(Mul x y, Add (MulR x y) y) => Mul (S x) y

Defined in Data.Repa.Scalar.Singleton.Nat

Associated Types

type MulR (S x) y :: N

Methods

mul :: Nat (S x) -> Nat y -> Nat (MulR (S x) y)

Literals

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