Add list_case, a definition for match on list

1 files changed, 9 insertions, 0 deletions

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.