From 6ce40f46d93a3dabd7ae01593a69702f2e7569ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 29 Apr 2016 21:18:00 +0200
Subject: [PATCH] Heterogeneous lists.

---
 theories/hlist.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 theories/hlist.v

diff --git a/theories/hlist.v b/theories/hlist.v
new file mode 100644
index 00000000..a0c70708
--- /dev/null
+++ b/theories/hlist.v
@@ -0,0 +1,18 @@
+From stdpp Require Import base.
+
+(* Not using [list Type] in order to avoid universe inconsistencies *)
+Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
+
+Inductive hlist : tlist → Type :=
+  | hnil : hlist tnil
+  | hcons {A As} : A → hlist As → hlist (tcons A As).
+
+Fixpoint himpl (As : tlist) (B : Type) : Type :=
+  match As with tnil => B | tcons A As => A → himpl As B end.
+
+Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
+  (fix go As xs :=
+    match xs in hlist As return himpl As B → B with
+    | hnil => λ f, f
+    | hcons A As x xs => λ f, go As xs (f x)
+    end) _ xs f.
-- 
GitLab