idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Typo fix in Data/Vect/Properties/Fin.idr

Browse Source
This commit is contained in:
Jason Hemann 2024-03-08 12:31:16 -05:00 committed by G. Allais
parent 809319fe8f
commit e4337c118b
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/contrib/Data/Vect/Properties/Fin.idr
View File

@ -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)