Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Fin

Description

A singleton-esque type for representing members of finite sets.

Synopsis

Documentation

data Fin :: N -> * where Source #

Constructors

FZ :: Fin (S n)
FS :: !(Fin n) -> Fin (S n)

Instances

Read1 N Fin Source #
Methods readsPrec1 :: Int -> ReadS (Some Fin f) Source #
Show1 N Fin Source #
Methods showsPrec1 :: Int -> f a -> ShowS Source # show1 :: f a -> String Source #
Ord1 N Fin Source #
Methods compare1 :: f a -> f a -> Ordering Source # (<#) :: f a -> f a -> Bool Source # (>#) :: f a -> f a -> Bool Source # (<=#) :: f a -> f a -> Bool Source # (>=#) :: f a -> f a -> Bool Source #
Eq1 N Fin Source #
Methods eq1 :: f a -> f a -> Bool Source # neq1 :: f a -> f a -> Bool Source #
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source #	A `Fin n` is a `Witness` that `n >= 1`. That is, `Pred n` is well defined.
Associated Types type WitnessC (ØC :: Constraint) ((~) N (S n') n :: Constraint) (Fin n) :: Constraint Source # Methods (\\) :: ØC => ((N ~ S n') n -> r) -> Fin n -> r Source #
(Known N Nat n, Pos n) => Bounded (Fin n) Source #
Methods minBound :: Fin n # maxBound :: Fin n #
(Known N Nat n, Pos n) => Enum (Fin n) Source #
Methods succ :: Fin n -> Fin n # pred :: Fin n -> Fin n # toEnum :: Int -> Fin n # fromEnum :: Fin n -> Int # enumFrom :: Fin n -> [Fin n] # enumFromThen :: Fin n -> Fin n -> [Fin n] # enumFromTo :: Fin n -> Fin n -> [Fin n] # enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n] #
Eq (Fin n) Source #
Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
Ord (Fin n) Source #
Methods compare :: Fin n -> Fin n -> Ordering # (<) :: Fin n -> Fin n -> Bool # (<=) :: Fin n -> Fin n -> Bool # (>) :: Fin n -> Fin n -> Bool # (>=) :: Fin n -> Fin n -> Bool # max :: Fin n -> Fin n -> Fin n # min :: Fin n -> Fin n -> Fin n #
Show (Fin n) Source #
Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #
type WitnessC ØC ((~) N (S n') n) (Fin n) Source #
type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n)

elimFin :: (forall x. p (S x)) -> (forall x. Fin x -> p x -> p (S x)) -> Fin n -> p n Source #

fins :: Nat n -> [Fin n] Source #

Gives the list of all members of the finite set of size n.

fin :: Fin n -> Int Source #

finZ :: Fin Z -> Void Source #

There are no members of Fin Z.

weaken :: Fin n -> Fin (S n) Source #

without :: Fin n -> Fin n -> Maybe (Fin (Pred n)) Source #

Map a finite set to a lower finite set without one of its members.

finNat :: Fin x -> Some Nat Source #

Take a Fin to an existentially quantified Nat.