Some recursive Fin functions (#1077)

Found myself needing these when using these as variables in well-scoped lambda terms.
agda · Nov 9, 2023 · 4de6b69 · 4de6b69
1 parent f8d6fcf
commit 4de6b69
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/Cubical/Data/Fin/Recursive/Base.agda b/Cubical/Data/Fin/Recursive/Base.agda
@@ -32,3 +32,7 @@ elim
   → (fn : Fin k) → P fn
 elim {k = suc k} P fz fs zero = fz
 elim {k = suc k} P fz fs (suc x) = fs x (elim P fz fs x)
+
+toℕ : Fin k → ℕ
+toℕ {suc k}   zero  = zero
+toℕ {suc k} (suc n) = suc (toℕ n)
diff --git a/Cubical/Data/Fin/Recursive/Properties.agda b/Cubical/Data/Fin/Recursive/Properties.agda
@@ -179,6 +179,10 @@ toFin : (n : ℕ) → Fin (suc n)
 toFin zero = zero
 toFin (suc n) = suc (toFin n)
 
+toFin< : (m : ℕ) → m < n → Fin n
+toFin< {suc n} zero 0<sn = zero
+toFin< {suc n} (suc m) m<n = suc (toFin< m m<n)
+
 inject<#toFin : ∀(i : Fin n) → inject< (≤-refl (suc n)) i # toFin n
 inject<#toFin {suc n} zero = _
 inject<#toFin {suc n} (suc i) = inject<#toFin {n} i