Fin Agda Idirs Agda Idris toℕ : Fin n → ℕ finToNat : Fin n -> Nat finToInteger : Fin n -> Integer fromℕ< : m ℕ.< n → Fin n natToFinLT : (x : Nat) -> {0 n : Nat} -> {auto 0 prf : x LT n} -> Fin n natToFinLt : (x : Nat) -> {0 n : Nat} ->{auto 0 prf : So (x < n)} -> Fin n natToFin : Nat -> (n : Nat) -> Maybe (Fin n) inject₁ : Fin n → Fin (suc n) weaken : Fin n -> Fin (S n) _↑ʳ_ : ∀ {m} n → Fin m → Fin (n ℕ.+ m) weakenN : (0 n : Nat) -> Fin m -> Fin (m + n) _inject≤ : Fin m → m ℕ.≤ n → Fin n weakenLTE : Fin n -> LTE n m -> Fin m lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n) strengthen : ∀ (i : Fin n) → Fin′ (suc i) cast : .(m ≡ n) → Fin m → Fin n coerce : {n : Nat} -> (0 eq : m = n) -> Fin m -> Fin n show : ∀ {n} → Fin n → String Show (Fin n) where show = show . finToInteger Only in Idris Agda Idris natToFin : Nat -> (n : Nat) -> Maybe (Fin n) finFromInteger fromInteger : (x : Integer) -> {auto 0 prf : So (integerLessThanNat x n)} -> Fin n integerLessThanNat : Integer -> Nat -> Bool restrict : (n : Nat) -> Integer -> Fin (S n) Eq (Fin n) where x == y = finToNat x == finToNat y shift : (m : Nat) -> Fin n -> Fin (m + n) allFins : (n : Nat) -> List (Fin n) allFins : (n : Nat) -> List1 (Fin (S n))