hlist.v 965 Bytes
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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.
19
20
21
22
23
24
25
26
27
28
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.