From 5c1f62d73ed4ef91452f86e885a58018d8968dff 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.

---
 _CoqProject     |  1 +
 prelude/hlist.v | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 prelude/hlist.v

diff --git a/_CoqProject b/_CoqProject
index 2793abada..570535e83 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,6 +35,7 @@ prelude/decidable.v
 prelude/list.v
 prelude/error.v
 prelude/functions.v
+prelude/hlist.v
 algebra/option.v
 algebra/cmra.v
 algebra/cmra_big_op.v
diff --git a/prelude/hlist.v b/prelude/hlist.v
new file mode 100644
index 000000000..1f307b062
--- /dev/null
+++ b/prelude/hlist.v
@@ -0,0 +1,18 @@
+From iris.prelude 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