------------------------------------------------------------------------ -- The Agda standard library -- -- Finite sets ------------------------------------------------------------------------ -- Note that elements of Fin n can be seen as natural numbers in the -- set {m | m < n}. The notation "m" in comments below refers to this -- natural number view. module Data.Fin where open import Data.Nat as Nat using (ℕ; zero; suc; z≤n; s≤s) renaming ( _+_ to _N+_; _∸_ to _N∸_ ; _≤_ to _N≤_; _≥_ to _N≥_; _<_ to _N<_; _≤?_ to _N≤?_) open import Function import Level open import Relation.Nullary.Decidable open import Relation.Binary ------------------------------------------------------------------------ -- Types -- Fin n is a type with n elements. data Fin : ℕ → Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} (i : Fin n) → Fin (suc n) -- A conversion: toℕ "n" = n. toℕ : ∀ {n} → Fin n → ℕ toℕ zero = 0 toℕ (suc i) = suc (toℕ i) -- A Fin-indexed variant of Fin. Fin′ : ∀ {n} → Fin n → Set Fin′ i = Fin (toℕ i) ------------------------------------------------------------------------ -- Conversions -- toℕ is defined above. -- fromℕ n = "n". fromℕ : (n : ℕ) → Fin (suc n) fromℕ zero = zero fromℕ (suc n) = suc (fromℕ n) -- fromℕ≤ {m} _ = "m". fromℕ≤ : ∀ {m n} → m N< n → Fin n fromℕ≤ (Nat.s≤s Nat.z≤n) = zero fromℕ≤ (Nat.s≤s (Nat.s≤s m≤n)) = suc (fromℕ≤ (Nat.s≤s m≤n)) -- # m = "m". #_ : ∀ m {n} {m