From 5efc05b747b6edcdbd2c298855d9de53d8567369 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 13 Jun 2018 15:18:28 -0400 Subject: Add PrimitiveHList, PrimitiveProd --- src/Util/PrimitiveHList.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 src/Util/PrimitiveHList.v (limited to 'src/Util/PrimitiveHList.v') diff --git a/src/Util/PrimitiveHList.v b/src/Util/PrimitiveHList.v new file mode 100644 index 000000000..356861ebe --- /dev/null +++ b/src/Util/PrimitiveHList.v @@ -0,0 +1,18 @@ +Require Import Coq.Lists.List. +Require Import Crypto.Util.PrimitiveProd. + +Fixpoint hlist {A} (P : A -> Type) (ls : list A) : Type + := match ls return Type with + | nil => unit + | cons x xs => P x * @hlist A P xs + end%type. +Fixpoint split_list {A P} (ls : list (@sigT A P)) : { ls : list A & hlist P ls } + := match ls with + | nil => existT _ nil tt + | cons x xs => let 'existT ls' hls' := @split_list A P xs in existT _ (cons (projT1 x) ls') (projT2 x, hls') + end. +Fixpoint combine_hlist {A P} (ls : list A) : hlist P ls -> list (@sigT A P) + := match ls return hlist P ls -> _ with + | nil => fun _ => nil + | cons x xs => fun '(Px, Pxs) => existT P x Px :: @combine_hlist A P xs Pxs + end. -- cgit v1.2.3