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

POrd Nat (KProxy Nat)

SEq Nat (KProxy Nat)

PEq Nat (KProxy Nat)

SDecide Nat (KProxy Nat)

SingKind Nat (KProxy Nat)

Typeable (Nat -> *) Fin

Typeable (Nat -> *) Signed

Typeable (Nat -> *) Unsigned

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$)

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:-$$)

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:*$$)

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:+$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:-$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:*$)

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$)

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

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

type Compare Nat a b = CmpNat a b

type (:==) Nat a b = (==) Nat a b

type Apply Nat Nat ((:+$$) l1) l0 = (:+$$$) l1 l0

type Apply Nat Nat ((:-$$) l1) l0 = (:-$$$) l1 l0

type Apply Nat Nat ((:*$$) l1) l0 = (:*$$$) l1 l0

type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0

type DemoteRep Nat (KProxy Nat) = Integer

type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0

type Apply (TyFun Nat Nat -> *) Nat (:-$) l0 = (:-$$) l0

type Apply (TyFun Nat Nat -> *) Nat (:*$) l0 = (:*$$) l0

type Apply (TyFun Nat Nat -> *) Nat (:^$) l0 = (:^$$) l0