diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Coercion.tex | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/doc/Coercion.tex b/doc/Coercion.tex index 13e4cd4473..69e81f6aa3 100644 --- a/doc/Coercion.tex +++ b/doc/Coercion.tex @@ -221,6 +221,22 @@ coercion between {\class$_1$} and {\class$_2$}. \item {\tt Identity Coercion Local {\ident}:{\ident$_1$} >-> {\ident$_2$}.} \\ Idem but locally to the current section. +\item {\tt SubClass {\ident} := {\type}.} \\ +\comindex{SubClass} + If {\type} is a class +{\ident'} applied to some arguments then {\ident} is defined and an +identity coercion of name {\tt Id\_{\ident}\_{\ident'}} is +declared. Otherwise said, this is an abbreviation for + +{\tt Definition {\ident} := {\type}.} + + followed by + +{\tt Identity Coercion Id\_{\ident}\_{\ident'}:{\ident} >-> {\ident'}}. + +\item {\tt Local SubClass {\ident} := {\type}.} \\ +Same as before but locally to the current section. + \end{Variants} \asection{Displaying Available Coercions} |