diff options
| author | herbelin | 2002-10-19 06:49:53 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-19 06:49:53 +0000 |
| commit | fd8a68ce203bdd5daadcc0302b13a0b3ea0db1b1 (patch) | |
| tree | 5eb7f94306b62ba1d6770d1e5de5a5f25c92dd3d /doc | |
| parent | 428210f7e52263b6445d06ef2c0de74fa88f8300 (diff) | |
Ajout d'infixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3158 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/newsyntax.tex | 30 |
1 files changed, 24 insertions, 6 deletions
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex index 035d3d8bd2..e02a1b5b67 100644 --- a/doc/newsyntax.tex +++ b/doc/newsyntax.tex @@ -561,13 +561,31 @@ $identificateur$ & $module$ & $infixe/préfixe$ & $précédence$ \\ \texttt{eq _} & $Logic$ & = & 50 \\ \texttt{eqT _} & $Logic_Type$ & = & 50 \\ \texttt{identityT _} & $Data_Type$ & = & 50 \\ -\texttt{plus} & $Peano$ & + & 40\,L \\ +\texttt{le} & $Peano$ & $<=$ & 50 \\ +\texttt{lt} & $Peano$ & $<$ & 50 \\ +\texttt{ge} & $Peano$ & $>=$ & 50 \\ +\texttt{gt} & $Peano$ & $>$ & 50 \\ +\texttt{Zle} & $zarith_aux$ & $<=$ & 50 \\ +\texttt{Zlt} & $zarith_aux$ & $<$ & 50 \\ +\texttt{Zge} & $zarith_aux$ & $>=$ & 50 \\ +\texttt{Zgt} & $zarith_aux$ & $>$ & 50 \\ +\texttt{Rle} & $Rdefinitions$ & $<=$ & 50 \\ +\texttt{Rlt} & $Rdefinitions$ & $<$ & 50 \\ +\texttt{Rge} & $Rdefinitions$ & $>=$ & 50 \\ +\texttt{Rgt} & $Rdefinitions$ & $>$ & 50 \\ +\texttt{plus} & $Peano$ & + & 40\,L \\ \texttt{Zplus} & $fast_integer$ & + & 40\,L \\ -\texttt{minus} & $Minus$ & - & 40\,L \\ -\texttt{Zminus} & $zarith_aux$ & - & 40\,L \\ +\texttt{Rplus} & $fast_integer$ & + & 40\,L \\ +\texttt{minus} & $Minus$ & - & 40\,L \\ +\texttt{Zminus} & $zarith_aux$ & - & 40\,L \\ +\texttt{Rminus} & $Rdefinitions$ & - & 40\,L \\ \texttt{Zopp} & $fast_integer$ & - & 40\,L \\ -\texttt{mult} & $Peano$ & * & 30\,L \\ -\texttt{Zmult} & $fast_integer$ & * & 30\,L +\texttt{Ropp} & $Rdefinitions$ & - & 40\,L \\ +\texttt{mult} & $Peano$ & * & 30\,L \\ +\texttt{Zmult} & $fast_integer$ & * & 30\,L \\ +\texttt{Rmult} & $Rdefinitions$ & * & 30\,L \\ +\texttt{Rdiv} & $Rdefinitions$ & / & 30\,L \\ +\texttt{pow} & $Rfunctions$ & \hat & 20\,L \\ \end{array} $$ @@ -647,7 +665,7 @@ Même problème pour l'entier de Specialize (ou virer Specialize ?) ? \verb=EAuto= : deux syntaxes différentes pour la recherche en largeur et en profondeur ? Quelle recherche par défaut ? -\section*{Remarques p\^ele-m\^ele (HH)} +\section*{Remarques pêle-mêle (HH)} Renommer Variable/Hypothesis hors section en Parameter/Axiom. |