diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index f32793f..50a4d1e 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. -From mathcomp Require Import seq choice fintype. +From mathcomp Require Import seq choice fintype path. Set Implicit Arguments. Unset Strict Implicit. @@ -208,6 +208,10 @@ Lemma allpairs_tupleP f t (u : m.-tuple U) : @size rT (allpairs f t u) == n * m. Proof. by rewrite size_allpairs !size_tuple. Qed. Canonical allpairs_tuple f t u := Tuple (allpairs_tupleP f t u). +Lemma sort_tupleP r t : size (sort r t) == n. +Proof. by rewrite size_sort size_tuple. Qed. +Canonical sort_tuple r t := Tuple (sort_tupleP r t). + Definition thead (u : n.+1.-tuple T) := tnth u ord0. Lemma tnth0 x t : tnth [tuple of x :: t] ord0 = x. |