Add tuple hd and tl

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index aca78cd5a..c030a03f8 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -17,6 +17,19 @@ Definition tuple T n : Type :=
   | S n' => tuple' T n'
   end.
 
+Definition tl' {T n} : tuple' T (S n) -> tuple' T n := @fst _ _.
+Definition tl {T n} : tuple T (S n) -> tuple T n :=
+  match n with
+  | O => fun _ => tt
+  | S n' => @tl' T n'
+  end.
+Definition hd' {T n} : tuple' T n -> T :=
+  match n with
+  | O => fun x => x
+  | S n' => @snd _ _
+  end.
+Definition hd {T n} : tuple T (S n) -> T := @hd' _ _.
+
 Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
   match n with
   | 0 => fun x => (x::nil)%list