From 9a367b2bfed76b0f2ac6db26ea0408227ad93230 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Jun 2019 11:11:12 +0100
Subject: Coq: add concatenation operator for polymorphic vectors

---
 lib/coq/Sail2_values.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 94f93736..bd22371a 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -2300,6 +2300,18 @@ simpl.
 auto with zarith.
 Qed.
 
+Definition vec_concat {T m n} (v : vec T m) (w : vec T n) : vec T (m + n).
+refine (existT _ (projT1 v ++ projT1 w) _).
+destruct v.
+destruct w.
+simpl.
+unfold length_list in *.
+rewrite <- e, <- e0.
+rewrite app_length.
+rewrite Nat2Z.inj_add.
+reflexivity.
+Defined.
+
 Lemma skipn_length {A n} {l: list A} : (n <= List.length l -> List.length (skipn n l) = List.length l - n)%nat.
 revert l.
 induction n.
-- 
cgit v1.2.3