summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Thu, 19 Jan 1995 19:46:49 +0100 | |

changeset 867 | e1a654c29b05 |

parent 866 | 2d3d020eef11 |

child 868 | 452f1e6ae3bc |

some cosmetic changes

--- a/doc-src/Ref/defining.tex Thu Jan 19 16:05:21 1995 +0100 +++ b/doc-src/Ref/defining.tex Thu Jan 19 19:46:49 1995 +0100 @@ -188,12 +188,19 @@ \verb!x<(y::nat)!. \end{warn} -Isabelle's representation of mathematical languages is based on the simply -typed $\lambda$-calculus\index{lambda calc@$\lambda$-calculus}. All user -defined logical types, namely those of class \cldx{logic}, refer to the -nonterminal {\tt logic}. Thus they are automatically equipped with a basic -syntax of types, identifiers, variables, parentheses, $\lambda$-abstractions -and applications. +\subsection{Logical types and default syntax}\label{logical-types} +\index{lambda calc@$\lambda$-calculus} + +Isabelle's representation of mathematical languages is based on the +simply typed $\lambda$-calculus. All logical types, namely those of +class \cldx{logic}, are automatically equipped with a basic syntax of +types, identifiers, variables, parentheses, $\lambda$-abstraction and +application. +\begin{warn} + Isabelle combines the syntaxes for all types of class \cldx{logic} by + mapping all those types to the single nonterminal $logic$. Thus all + productions of $logic$, in particular $id$, $var$ etc, become available. +\end{warn} \subsection{Lexical matters} @@ -488,11 +495,6 @@ is sensible only if~$c$ is an identifier. Otherwise you will be unable to write terms involving~$c$. -\medskip -There is something artificial about the representation of productions as -mixfix declarations, but it is convenient, particularly for simple theory -extensions. - \subsection{Example: arithmetic expressions} \index{examples!of mixfix declarations} @@ -539,6 +541,12 @@ {\out exp = "-" exp[3] => "-" (3)} \end{ttbox} +Note that because {\tt exp} is not of class {\tt logic}, it has been retained +as a separate nonterminal. This also entails that the syntax does not provide +for identifiers or paranthesized expressions. Normally you would also want to +add the declaration {\tt arities exp :: logic} and use {\tt consts} instead +of {\tt syntax}. Try this as an exercise and study the changes in the +grammar. \subsection{The mixfix template} Let us now take a closer look at the string $template$ appearing in mixfix