From 17291b8a3374266872e15c442adfd461dc3f65be Mon Sep 17 00:00:00 2001
From: Joe Hendrix <jhendrix@galois.com>
Date: Thu, 20 Apr 2017 12:02:41 -0700
Subject: [PATCH] refactor(library/data/vector): allow tail to accept empty
 vector.

---
 library/data/vector.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/data/vector.lean b/library/data/vector.lean
index 7fe2f6614b..151583bb4d 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -38,8 +38,8 @@ def head : vector α (nat.succ n) → α
 theorem head_cons (a : α) : Π (v : vector α n), head (a :: v) = a
 | ⟨ l, h ⟩ := rfl
 
-def tail : vector α (succ n) → vector α n
-| ⟨ [],     h ⟩ := by contradiction
+def tail : vector α n → vector α (n - 1)
+| ⟨ [],     h ⟩ := ⟨ [], congr_arg pred h ⟩
 | ⟨ a :: v, h ⟩ := ⟨ v, congr_arg pred h ⟩
 
 theorem tail_cons (a : α) : Π (v : vector α n), tail (a :: v) = v