From 83ecdb1befe209f91e5b49cdd0ff0b5dfa6b7cc2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 7 Nov 2016 13:19:16 -0500 Subject: Add tuple hd and tl --- src/Util/Tuple.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/Tuple.v') 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 -- cgit v1.2.3