diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-22 23:33:49 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-22 23:33:49 -0500 |
commit | 9f0102d8c0c2a35cb14d7ebf9020b74ea4bcccbe (patch) | |
tree | 4f9afc3dabaf033c62b56325d664c824c674b5d8 /src/Util | |
parent | 349faa231f8b2c94d3b5363fdfabac523c55e647 (diff) |
Add hlistP
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/HList.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 57507eeb5..1a724f84b 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 hlistP' T n (f : T -> Prop) : tuple' T n -> Prop := + match n return tuple' _ n -> Prop with + | 0 => fun T => f T + | S n' => fun Ts => (hlistP' T n' f (fst Ts) /\ f (snd Ts))%type + end. +Global Arguments hlistP' {T n} f _. + +Definition hlistP {T n} (f : T -> Prop) : forall (Ts : tuple T n), Prop := + match n return tuple _ n -> Prop with + | 0 => fun _ => True + | S n' => @hlistP' 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 |