From 6683a2147ff662af688a667db911f44f7925442f Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Sat, 27 Jun 2020 15:54:35 +0100 Subject: [PATCH] Export the `lengthCorrect` proof, as users might want to use it Change the `len` to be irrelevant, as it's uniquely determined by matching on the input vector --- libs/base/Data/Vect.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr index 758ac52bf..97325f13e 100644 --- a/libs/base/Data/Vect.idr +++ b/libs/base/Data/Vect.idr @@ -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