Data.Type.Fin

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

Documentation

data Fin :: N -> * where

Constructors

FZ :: Fin (S n)

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

Instances

(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n)

A Fin n is a Witness that n >= 1.

That is, Pred n is well defined.

Eq (Fin n)

Ord (Fin n)

Show (Fin n)

type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n)

fins :: Nat n -> [Fin n]

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

fin :: Fin n -> Int

finZ :: Fin Z -> Void

There are no members of Fin Z.

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

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

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

class x <= y where

Methods

weakenN :: Fin x -> Fin y

Instances

x <= x

(<=) x y => x <= (S y)

finNat :: Fin x -> Some Nat

Take a Fin to an existentially quantified Nat.