diff options
| author | Antonio Nikishaev | 2020-04-08 00:32:35 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-08 01:34:03 +0400 |
| commit | bfd4b28b835e6918d7f4dea848c8b94f4c1c6f7f (patch) | |
| tree | 5eda6b55c8907856c311c798b8ff5dc8fb7ca82c /mathcomp/ssreflect/tuple.v | |
| parent | 815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 (diff) | |
fix typos in documentation: formulae
Diffstat (limited to 'mathcomp/ssreflect/tuple.v')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index ed55b08..c682a20 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -18,7 +18,7 @@ Unset Printing Implicit Defensive. (* [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. *) |