type-combinators-0.2.2.0: A collection of data types for type-level programming

CopyrightCopyright (C) 2015 Kyle Carter
LicenseBSD3
MaintainerKyle Carter <kylcarte@indiana.edu>
Stabilityexperimental
PortabilityRankNTypes
Safe HaskellNone
LanguageHaskell2010

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 
Show2 N N IFin Source 
Ord2 N N IFin Source 
Eq2 N N IFin Source 
Show1 N (IFin x) Source 
Ord1 N (IFin x) Source 
Eq1 N (IFin x) 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.

Eq (IFin x y) Source 
Ord (IFin x y) Source 
Show (IFin x y) Source 
type WitnessC ØC ((~) N (S x') x) (IFin x y) = (~) N x' (Pred x) Source 

class LTC x y => LessEq x y where Source

Associated Types

type LTC x y :: Constraint Source

Methods

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

Instances

LessEq Z y Source 
((~) N y (S (Pred y)), LessEq x (Pred y)) => LessEq (S x) y 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