Data.Fin

v0.1.0 • Finite Sets

Finite sets (inductive types parameterized by natural numbers).

Types

Fin :: Nat -> *

Finite sets. Fin N is a type with exactly N inhabitants. It is an inductive type indexed by a natural number N.

Implementation 
data Fin N = FZero N | FSucc N (Fin N)
Usage 
z = FZero (Succ Zero) -- 0 in Fin 1
s = FSucc (Succ Zero) (FZero Zero) -- 1 in Fin 2