------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets defined using the reflexive-transitive closure, Star
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Fin where

open import Data.Star.Nat as ℕ using (ℕ)
open import Data.Star.Pointer using (Any; this; that)
open import Data.Unit.Base using (⊤; tt)

-- 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