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.Indexed

Description

A singleton-esque type for representing members of finite sets, indexed by its Nat value.

Synopsis

Documentation

data IFin :: N -> N -> * where Source #

Constructors

IFZ :: IFin (S x) Z
IFS :: !(IFin x y) -> IFin (S x) (S y)

Instances

Read2 N N IFin Source #
Methods readsPrec2 :: Int -> ReadS (Some2 IFin k f) Source #
Show2 N N IFin Source #
Methods showsPrec2 :: Int -> f a b -> ShowS Source # show2 :: f a b -> String Source #
Ord2 N N IFin Source #
Methods compare2 :: f a b -> f a b -> Ordering Source # (<##) :: f a b -> f a b -> Bool Source # (>##) :: f a b -> f a b -> Bool Source # (<=##) :: f a b -> f a b -> Bool Source # (>=##) :: f a b -> f a b -> Bool Source #
Eq2 N N IFin Source #
Methods eq2 :: f a b -> f a b -> Bool Source # neq2 :: f a b -> f a b -> Bool Source #
Show1 N (IFin x) Source #
Methods showsPrec1 :: Int -> f a -> ShowS Source # show1 :: f a -> String Source #
Ord1 N (IFin x) 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 (IFin x) Source #
Methods eq1 :: f a -> f a -> Bool Source # neq1 :: f a -> f a -> Bool Source #
(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y) Source #	An `IFin x y` is a `Witness` that `x >= 1`. That is, `Pred x` is well defined.
Associated Types type WitnessC (ØC :: Constraint) ((~) N (S x') x :: Constraint) (IFin x y) :: Constraint Source # Methods (\\) :: ØC => ((N ~ S x') x -> r) -> IFin x y -> r Source #
Eq (IFin x y) Source #
Methods (==) :: IFin x y -> IFin x y -> Bool # (/=) :: IFin x y -> IFin x y -> Bool #
Ord (IFin x y) Source #
Methods compare :: IFin x y -> IFin x y -> Ordering # (<) :: IFin x y -> IFin x y -> Bool # (<=) :: IFin x y -> IFin x y -> Bool # (>) :: IFin x y -> IFin x y -> Bool # (>=) :: IFin x y -> IFin x y -> Bool # max :: IFin x y -> IFin x y -> IFin x y # min :: IFin x y -> IFin x y -> IFin x y #
Show (IFin x y) Source #
Methods showsPrec :: Int -> IFin x y -> ShowS # show :: IFin x y -> String # showList :: [IFin x y] -> ShowS #
type WitnessC ØC ((~) N (S x') x) (IFin x y) Source #
type WitnessC ØC ((~) N (S x') x) (IFin x y) = (~) N x' (Pred x)

class LTC x y => LessEq x y where Source #

Minimal complete definition

liftIFin

Associated Types

type LTC x y :: Constraint Source #

Methods

liftIFin :: IFin x z -> IFin y z Source #

Instances

LessEq Z y Source #
Associated Types type LTC (Z :: N) (y :: N) :: Constraint Source # Methods liftIFin :: IFin Z z -> IFin y z Source #
((~) N y (S (Pred y)), LessEq x (Pred y)) => LessEq (S x) y Source #
Associated Types type LTC (S x :: N) (y :: N) :: Constraint Source # Methods liftIFin :: IFin (S x) z -> IFin y z Source #

ifinZ :: IFin Z x -> Void Source #

weaken :: IFin x y -> IFin (S x) y Source #

ifinNat :: IFin x y -> Nat y Source #

ifinVal :: IFin x y -> Int Source #

onIFinPred :: (forall x. IFin m x -> IFin n x) -> IFin (S m) y -> IFin (S n) y Source #