diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-08 11:26:37 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-08 11:26:37 -0500 |
commit | 74093540ce9a99f727696b90b20b8578b71f8d55 (patch) | |
tree | 5a85fe8423aef5bee91e7bce49af327b3f009a75 /src/Util | |
parent | 853821e4374050d5a770ee623b24a7bf15e288ae (diff) |
Add HList.const
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/HList.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v index 0ebb4cdce..aacefe8f3 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -19,6 +19,17 @@ Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := | S n' => @hlist' 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 _ + | S n' => fun _ => (@const' T n' F _ v, v _) + end xs. +Definition 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 _ => tt + | S n' => fun xs => @const' T n' F xs v + end xs. + (* tuple map *) Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall {ts : tuple' A n}, hlist' F ts -> tuple' B n := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with |