Commit 361c9fbf authored by Ralf Jung's avatar Ralf Jung

use \bnfdef

parent 9656f4b1
...@@ -93,13 +93,13 @@ Elements of $\SigAx$ are ranged over by $\sigax$. ...@@ -93,13 +93,13 @@ Elements of $\SigAx$ are ranged over by $\sigax$.
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$): Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
\begin{align*} \begin{align*}
\type ::={}& \type \bnfdef{}&
\sigtype \mid \sigtype \mid
1 \mid 1 \mid
\type \times \type \mid \type \times \type \mid
\type \to \type \type \to \type
\\[0.4em] \\[0.4em]
\term, \prop, \pred ::={}& \term, \prop, \pred \bnfdef{}&
\var \mid \var \mid
\sigfn(\term_1, \dots, \term_n) \mid \sigfn(\term_1, \dots, \term_n) \mid
() \mid () \mid
......
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