diff options
author | Jason Gross <jagro@google.com> | 2018-06-13 15:18:28 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-06-13 15:18:28 -0400 |
commit | 5efc05b747b6edcdbd2c298855d9de53d8567369 (patch) | |
tree | efbc78fc6fc158e4abc0e326e3afc93bd38ece84 /src/Util/PrimitiveHList.v | |
parent | b4a0f83c3d9853cd2594bfb3f88adda5e783451e (diff) |
Add PrimitiveHList, PrimitiveProd
Diffstat (limited to 'src/Util/PrimitiveHList.v')
-rw-r--r-- | src/Util/PrimitiveHList.v | 18 |
1 files changed, 18 insertions, 0 deletions
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. |