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

Merge pull request #372 from ohad/export-length-correct

Browse Source 
Export the `lengthCorrect` proof, as users might want to use it
This commit is contained in:
Ohad Kammar 2020-06-27 16:21:04 +01:00 committed by GitHub
commit f31318f5e6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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