Commit 6ce40f46 authored by Robbert Krebbers's avatar Robbert Krebbers

Heterogeneous lists.

parent 7e6955cd
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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment