aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Setoid.tex
diff options
context:
space:
mode:
authorGravatar staffehn <fdsteffahn@gmail.com>2017-09-03 16:27:25 +0200
committerGravatar GitHub <noreply@github.com>2017-09-03 16:27:25 +0200
commit97053f19094b5e4585e4f466e6c7a43fc1af535d (patch)
tree2ca434c0a638e1bc75aaa67272e4e5e0d8f0e125 /doc/refman/Setoid.tex
parent3072bd9d080984833f5eb007bf15c6e9305619e3 (diff)
2 Typos in 'Add Parametric Morphism' Documentation
Diffstat (limited to 'doc/refman/Setoid.tex')
-rw-r--r--doc/refman/Setoid.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 6c7928438..0c8cd408f 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -223,7 +223,7 @@ the following command.
\comindex{Add Parametric Morphism}
\begin{quote}
- \texttt{Add Parametric Morphism} ($x_1 : \T_!$) \ldots ($x_k : \T_k$)\\
+ \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) :
(\textit{f $t_1$ \ldots $t_n$})\\
\texttt{~with signature} \textit{sig}\\
\texttt{~as id}.\\