From cb0212005028c40263a9b90d384dba0be849ef39 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Mar 2017 11:30:12 +0100
Subject: [PATCH] inhabit vectors

---
 theories/vector.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/vector.v b/theories/vector.v
index a23e8c7a..13ed7220 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -355,3 +355,13 @@ Proof.
 Qed.
 Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.
 Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.
+
+(* Vectors can be inhabited. *)
+Global Instance vec_nil_inh T : Inhabited (vec T 0) := populate [#].
+
+Global Instance vec_inh T n : Inhabited T → Inhabited (vec T n).
+Proof.
+  intros HT. induction n; [apply _|].
+  destruct IHn as [v]. destruct HT as [x].
+  exact (populate (x:::v)).
+Qed.
-- 
GitLab