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

Read1 N Fin

Show1 N Fin

Ord1 N Fin

Eq1 N Fin

(~) 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)

elimFin :: (forall x. p (S x)) -> (forall x. Fin x -> p x -> p (S x)) -> Fin n -> p 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.

finNat :: Fin x -> Some Nat

Take a Fin to an existentially quantified Nat.