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

minor: fix spaces/alignment

Browse Source 
Thanks @gallais
This commit is contained in:
Ohad Kammar 2020-06-16 20:36:15 +01:00
parent 87d4411709
commit 9f643a2243
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libs/contrib/Data/List/TailRec.idr
View File

@ -19,9 +19,9 @@ module Data.List.TailRec
import Syntax.PreorderReasoning
import Syntax.WithProof
import Data.List
import Data.Vect
import Data.Nat
import Data.List
import Data.Vect
import Data.Nat
length_aux : List a -> Nat -> Nat
length_aux [] len = len
@ -35,9 +35,9 @@ export
length_ext : (xs : List a) -> Data.List.length xs = Data.List.TailRec.length xs
length_ext xs = Calc $
|~ Data.List.length xs
~~ Data.List.length xs + 0 ...( sym $ plusZeroRightNeutral $ Data.List.length xs )
~~ Data.List.TailRec.length_aux xs 0 ...( lemma 0 xs )
~~ Data.List.TailRec.length xs ...( Refl )
~~ Data.List.length xs + 0 ...( sym $ plusZeroRightNeutral $ Data.List.length xs )
~~ Data.List.TailRec.length_aux xs 0 ...( lemma 0 xs )
~~ Data.List.TailRec.length xs ...( Refl )
where
lemma : (n : Nat) -> (xs : List a) ->
Data.List.length xs + n = length_aux xs n