------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets defined in terms of Data.Star
------------------------------------------------------------------------

module Data.Star.Fin where

open import Data.Star
open import Data.Star.Nat as  using ()
open import Data.Star.Pointer
open import Data.Unit

-- Finite sets are undecorated pointers into natural numbers.

Fin :   Set
Fin = Any  _  )  _  )

-- "Constructors".

zero :  {n}  Fin (.suc n)
zero = this tt

suc :  {n}  Fin n  Fin (.suc n)
suc = that tt