sized-types-0.5.0: Sized types in Haskell using the GHC Nat kind.

Safe HaskellNone
LanguageHaskell98

Data.Sized.Fin

Description

Fin types

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

Maintainer: Andy Gill andygill@ku.edu Stability: unstable Portability: ghc

Synopsis

Documentation

data Fin n Source

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 Source

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

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

A list of all possible values of a type.

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

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 
type (==) Nat a b = EqNat a b 
type DemoteRep Nat (KProxy Nat) = Integer