Commit 46db392a authored by Robbert Krebbers's avatar Robbert Krebbers

More heterogeneous list stuff.

parent 28045c10
......@@ -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.
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