idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-11 21:37:48 +03:00
Code Issues Projects Releases Wiki Activity

[ base ] Properties of indexing after replaceAt were added for Vect

Browse Source
This commit is contained in:
Denis Buzdalov 2021-03-18 11:43:41 +03:00 committed by G. Allais
parent 941e3963fa
commit 0749165245
1 changed files with 14 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
libs/base/Data/Vect.idr
View File

@ -198,6 +198,20 @@ export
merge : Ord elem => Vect n elem -> Vect m elem -> Vect (n + m) elem
merge = mergeBy compare
-- Properties for functions in this section --
export
replaceAtSameIndex : (xs : Vect n a) -> (i : Fin n) -> (0 y : a) -> index i (replaceAt i y xs) = y
replaceAtSameIndex (_::_) FZ _ = Refl
replaceAtSameIndex (_::_) (FS _) _ = replaceAtSameIndex _ _ _
export
replaceAtDiffIndexPreserves : (xs : Vect n a) -> (i, j : Fin n) -> Not (i = j) -> (0 y : a) -> index i (replaceAt j y xs) = index i xs
replaceAtDiffIndexPreserves (_::_) FZ FZ co _ = absurd $ co Refl
replaceAtDiffIndexPreserves (_::_) FZ (FS _) _ _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS _) FZ _ _ = Refl
replaceAtDiffIndexPreserves (_::_) (FS z) (FS w) co y = replaceAtDiffIndexPreserves _ z w (co . cong FS) y
--------------------------------------------------------------------------------
-- Transformations
--------------------------------------------------------------------------------