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

Rename to reverseInvolutive

Browse Source
This commit is contained in:
Mathew Polzin 2021-01-06 08:45:44 -08:00
parent bc76809288
commit e9324fcd60
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/base/Data/List.idr
View File

@ -672,11 +672,11 @@ revAppend (v :: vs) ns
||| List reverse applied twice yields the identity function.
export
reverseInvolutory : (xs : List a) -> reverse (reverse xs) = xs
reverseInvolutory [] = Refl
reverseInvolutory (x :: xs) = rewrite revOnto [x] xs in
reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
reverseInvolutive [] = Refl
reverseInvolutive (x :: xs) = rewrite revOnto [x] xs in
rewrite sym (revAppend (reverse xs) [x]) in
cong (x ::) $ reverseInvolutory xs
cong (x ::) $ reverseInvolutive xs
export
dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l