# [isabelle] Isabelle operator precedence

Dear all,

while it is mostly "intuitive" I would like to have a clearer view of
operator precedence in Isabelle. Attached is what I quickly reverse-
engineered on a train ride on the long weekend. Is it correct? Is there
already any explicit information on this (beyond using
Isabelle -> Settings -> Display -> Show Brackets in PG)?

Thanks,

--
Holger


Attachment: isabelle-operator-precedence-cheat-sheet.pdf
Description: Adobe PDF document

\documentclass[a4paper]{article}

\usepackage{amssymb}
\usepackage{stmaryrd}

\title{Isabelle operator precedence: experimental cheat sheet}
\author{author}

\begin{document}

\begin{table}[h]
Operator precedence cheat sheet in Isabelle-HOL (quick and dirty ad-hoc reverse-engineered mostly on a train ride, no quality control at all). For discussion at Isabelle users list.
\begin{center}

\begin{tabular}{|l|l|l|}
\hline
Class & Symbol(s) & Weight\\
\hline
\hline function & function application, field dereference (record), nth (list) & \\
\hline type	    & set'' type constructor, list'' type constructor & \\
\hline function & $\cap$ (set) & \\
\hline function & $\cup$ (set), \# (list), @ (list), + (nat), Suc (nat) & 65 \\
\hline relation & = & \\
\hline relation & $\in$, $<$, $\le$ & 50 \\
\hline logic    & $\neg$ & \\
\hline logic    & $\wedge$ & 35 \\
\hline logic    & $\vee$ & 30 \\
\hline logic    & $\longrightarrow$, $\leftrightarrow$ & 25 \\
\hline type	    & $\Rightarrow$ & \\
\hline logic    & $\forall$, $\exists$ & \\
\hline term     & if .. then .. else & \\
\hline term     & $\lambda$ & \\
\hline term     & .. $\llparenthesis$ .. := .. $\rrparenthesis$ (record) & \\
\hline term     & let .. = .. in .. & \\
\hline metalogic & $\equiv$ & \\
\hline metalogic & $\Longrightarrow$ & \\
\hline metalogic & $\bigwedge$ & \\
\hline

\end{tabular}
\caption{Higher symbols have higher precedence. Weights given where known (grepping Isabelle sources for infixr''). Classes are my own interpretation.}
\end{center}
\end{table}

\paragraph{Note on classes:}

\begin{description}
\item[function] if it is a function (type constructors set'', list'' could also be seen as functions)
\item[relation] if it is a relation
\item[logic] if it is object logic
\item[term] term constructors
\item[metalogic] if it is meta logic
\end{description}

%\tableofcontents

\end{document}


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.