From e4337c118bda6ee6d7cd9746092cb911157d376f Mon Sep 17 00:00:00 2001 From: Jason Hemann Date: Fri, 8 Mar 2024 12:31:16 -0500 Subject: [PATCH] Typo fix in Data/Vect/Properties/Fin.idr --- libs/contrib/Data/Vect/Properties/Fin.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/contrib/Data/Vect/Properties/Fin.idr b/libs/contrib/Data/Vect/Properties/Fin.idr index dfaf4ad48..574ab38f5 100644 --- a/libs/contrib/Data/Vect/Properties/Fin.idr +++ b/libs/contrib/Data/Vect/Properties/Fin.idr @@ -35,7 +35,7 @@ finToElem {n } xs i with (finNonEmpty xs $ finNonZero i) finToElem {n = S n} (x :: xs) FZ | IsNonEmpty = Here finToElem {n = S n} (x :: xs) (FS i) | IsNonEmpty = There (finToElem xs i) -||| Analogus to `indexNaturality`, but morhisms can (irrelevantly) know the context +||| Analogus to `indexNaturality`, but morphisms can (irrelevantly) know the context export indexNaturalityWithElem : (i : Fin n) -> (xs : Vect n a) -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b) -> index i (mapWithElem xs f) = f (index i xs) (finToElem xs i)