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

Export the lengthCorrect proof, as users might want to use it

Browse Source 
Change the `len` to be irrelevant, as it's uniquely determined by
matching on the input vector
This commit is contained in:
Ohad Kammar 2020-06-27 15:54:35 +01:00
parent 574524d8de
commit 6683a2147f
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -23,8 +23,8 @@ length [] = 0
length (x::xs) = 1 + length xs
||| Show that the length function on vectors in fact calculates the length
private
lengthCorrect : (len : Nat) -> (xs : Vect len elem) -> length xs = len
export
lengthCorrect : (0 len : Nat) -> (xs : Vect len elem) -> length xs = len
lengthCorrect Z [] = Refl
lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl