diff options
| -rw-r--r-- | src/Util/Tuple.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index a68e7ffe8..a5b299ac0 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -40,6 +40,13 @@ Fixpoint rsnoc' T n {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S end. Global Arguments rsnoc' {T n} _ _. +Fixpoint cons' T n {struct n} : forall (y : T) (x : tuple' T n), tuple' T (S n) + := match n return forall (y : T) (x : tuple' T n), tuple' T (S n) with + | O => fun y x => (y, x) + | S n' => fun y x => (@cons' T n' y (fst x), snd x) + end. +Global Arguments cons' {T n} _ _. + Fixpoint assoc_right' {n T} {struct n} : tuple' T n -> rtuple' T n := match n return tuple' T n -> rtuple' T n with @@ -56,6 +63,22 @@ Definition assoc_right {n T} | S n' => @assoc_right' n' T end. +Fixpoint assoc_left' {n T} {struct n} + : rtuple' T n -> tuple' T n + := match n return rtuple' T n -> tuple' T n with + | 0 => fun x => x + | S n' => fun ts => let xs := @assoc_left' n' T (snd ts) in + let x := fst ts in + cons' x xs + end. + +Definition assoc_left {n T} + : rtuple T n -> tuple T n + := match n with + | 0 => fun x => x + | S n' => @assoc_left' n' T + 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 |