From 349faa231f8b2c94d3b5363fdfabac523c55e647 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 22 Nov 2016 17:40:07 -0500 Subject: Add rhlist --- src/Util/HList.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/HList.v') diff --git a/src/Util/HList.v b/src/Util/HList.v index 802ab1ed3..57507eeb5 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -20,6 +20,19 @@ Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := | S n' => @hlist' T n' f end. +Fixpoint rhlist' T n (f : T -> Type) : rtuple' T n -> Type := + match n return rtuple' _ n -> Type with + | 0 => fun T => f T + | S n' => fun Ts => (f (fst Ts) * rhlist' T n' f (snd Ts))%type + end. +Global Arguments rhlist' {T n} f _. + +Definition rhlist {T n} (f : T -> Type) : forall (Ts : rtuple T n), Type := + match n return rtuple _ n -> Type with + | 0 => fun _ => unit + | S n' => @rhlist' T n' f + end. + Fixpoint const' {T n F xs} (v : forall x, F x) : @hlist' T n F xs := match n return forall xs, @hlist' T n F xs with | 0 => fun _ => v _ -- cgit v1.2.3