Commit 6a9642c0 authored by Ralf Jung's avatar Ralf Jung

docs: improve structure

parent 7e5ea1fe
Pipeline #269 passed with stage
......@@ -74,8 +74,6 @@ Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type
Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$.
Elements of $\SigAx$ are ranged over by $\sigax$.
\section{Syntax}
\subsection{Grammar}\label{sec:grammar}
\paragraph{Syntax.}
......@@ -276,7 +274,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
}
\end{mathparpagebreakable}
\subsection{Timeless Propositions}
\subsection{Timeless propositions}
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertions about propositions, defined by the following judgment.
......@@ -285,7 +283,7 @@ This is a \emph{meta-level} assertions about propositions, defined by the follow
\ralf{Define a judgment that defines them.}
\subsection{Base logic}
\subsection{Proof rules}
\ralf{Go on checking below.}
The judgment $\vctx \mid \pfctx \proves \prop$ says that with free variables $\vctx$, proposition $\prop$ holds whenever all assumptions $\pfctx$ hold.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment