diff options
| author | Antonio Nikishaev | 2020-04-09 11:10:17 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-09 11:12:47 +0400 |
| commit | 31dec18a2539cfdac70fd87401db2b4b14d81d16 (patch) | |
| tree | d39377474f8db1b94df5118341c9588e106c37c4 | |
| parent | 7d6e46ec9c8067553e9a82b5345778f00cf3c1e9 (diff) | |
docs: more ".-tuple" fixes
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index c682a20..551dc77 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -13,12 +13,12 @@ Unset Printing Implicit Defensive. (* [tuple of s] == the tuple whose underlying sequence (value) is s. *) (* The size of s must be known: specifically, Coq must *) (* be able to infer a Canonical tuple projecting on s. *) -(* in_tuple s == the (size s)-tuple with value s. *) +(* in_tuple s == the (size s).-tuple with value s. *) (* [tuple] == the empty tuple. *) (* [tuple x1; ..; xn] == the explicit n.-tuple <x1; ..; xn>. *) (* [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound *) (* in E). *) -(* tcast Emn t == the m.-tuple t cast as an n-tuple using Emn : m = n. *) +(* tcast Emn t == the m.-tuple t cast as an n.-tuple using Emn : m = n.*) (* As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be *) (* applied to t : n.-tuple T; we provide a few specialized instances when *) (* avoids the need for a default value. *) |