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

Documentation

Peano natural numbers.

Constructors

Z
S N

Instances

data Nat n where Source

Peano natural number singletons.

Constructors

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

Instances

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
Add x (S y) => Add (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
(Mul x y, Add (MulR x y) y) => Mul (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