Data.Sized.Fin

Fin types

Copyright: (c) 2013 University of Kansas License: BSD3

Maintainer: Andy Gill [e-mail] Stability: unstable Portability: ghc

Documentation

data Fin n

Instances

SingI Nat a => Bounded (Fin a)

Enum (Fin a)

Eq (Fin n)

SingI Nat a => Integral (Fin a)

SingI Nat a => Num (Fin a)

Ord (Fin n)

SingI Nat a => Read (Fin a)

SingI Nat a => Real (Fin a)

Show (Fin a)

SingI Nat a => Ix (Fin a)

Typeable (Nat -> *) Fin

fromNat :: Sing (n :: Nat) -> Integer

corners :: forall i. Bounded i => (i, i)

universe :: (Bounded ix, Ix ix) => [ix]

A list of all possible values of a type.

size :: forall ix. (Bounded ix, Ix ix) => ix -> Int

module Data.Singletons

data Nat :: *

(Kind) This is the kind of type-level natural numbers.

Instances

KnownNat n => SingI Nat n

SEq Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

SingKind Nat (KProxy Nat)

Typeable (Nat -> *) Fin

Typeable (Nat -> *) Signed

Typeable (Nat -> *) Unsigned

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

type (==) Nat a b = EqNat a b

type DemoteRep Nat (KProxy Nat) = Integer