Skip to content

Commit

Permalink
Typo fix in Data/Vect/Properties/Fin.idr
Browse files Browse the repository at this point in the history
  • Loading branch information
jasonhemann authored Mar 8, 2024
1 parent 809319f commit b44860c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion libs/contrib/Data/Vect/Properties/Fin.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit b44860c

Please sign in to comment.