From 88665b911de5e774b969e3372ed977b061235a77 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 27 Mar 2018 09:11:06 -0400
Subject: Add list_case, a definition for match on list

---
 src/Util/ListUtil.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/Util/ListUtil.v')

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index ddb0d973e..68cc6a41f 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -11,6 +11,15 @@ Require Export Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 
+Definition list_case
+           {A} (P : list A -> Type) (N : P nil) (C : forall x xs, P (cons x xs))
+           (ls : list A)
+  : P ls
+  := match ls return P ls with
+     | nil => N
+     | cons x xs => C x xs
+     end.
+
 Create HintDb distr_length discriminated.
 Create HintDb simpl_set_nth discriminated.
 Create HintDb simpl_update_nth discriminated.
-- 
cgit v1.2.3