From 46db392ab6258185a44e44f49db09a0a8500e8c2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 18 Jun 2016 00:48:32 +0200
Subject: [PATCH] More heterogeneous list stuff.

---
 theories/hlist.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/hlist.v b/theories/hlist.v
index a0c70708..be1f20db 100644
--- a/theories/hlist.v
+++ b/theories/hlist.v
@@ -16,3 +16,13 @@ Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
     | hnil => λ f, f
     | hcons A As x xs => λ f, go As xs (f x)
     end) _ xs f.
+Coercion happly : himpl >-> Funclass.
+
+Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C :=
+  match As with
+  | tnil => f
+  | tcons A As => λ g x, hcompose f (g x)
+  end.
+
+Definition hinit {B} (y : B) : himpl tnil B := y.
+Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
-- 
GitLab