{-# OPTIONS --safe #-}

module Data.Fin where

open import Prelude

mutual
  data Fin⁰ : Type where

  data Fin⁺ (n : ℕ) : Type where
    fz : Fin⁺ n
    fs : Fin n → Fin⁺ n

  Fin : ℕ → Type
  Fin zero = Fin⁰
  Fin (suc n) = Fin⁺ n
    
private variable n : ℕ

f0 : Fin (suc n)
f0 = fz

f1 : Fin (suc (suc n))
f1 = fs f0


f2 : Fin (suc (suc (suc n)))
f2 = fs f1

f3 : Fin (suc (suc (suc (suc n))))
f3 = fs f2

f4 : Fin (suc (suc (suc (suc (suc n)))))
f4 = fs f3

module DiscreteFin where
  opaque
    _≡ᴮ_ : Fin n → Fin n → Bool
    _≡ᴮ_ {suc n} fz fz = true
    _≡ᴮ_ {suc n} fz (fs _) = false
    _≡ᴮ_ {suc n} (fs _) fz = false
    _≡ᴮ_ {suc n} (fs x) (fs y) = x ≡ᴮ y

    complete : ∀ (x : Fin n) → T (x ≡ᴮ x)
    complete {n = suc n} fz = tt
    complete {n = suc n} (fs x) = complete x

    sound : ∀ (x y : Fin n) → T (x ≡ᴮ y) → x ≡ y
    sound {n = suc _} fz fz xy = refl
    sound {n = suc _} (fs x) (fs y) xy = cong fs (sound x y xy)

instance
  opaque
    discreteFin : IsDiscrete (Fin n)
    discreteFin = record { _≟_ = from-bool-eq (record { DiscreteFin }) }