From 361c9fbf4a06d862e4350322c735005b3d54e0be Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 8 Mar 2016 09:46:41 +0100
Subject: [PATCH] use \bnfdef
---
docs/logic.tex | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/docs/logic.tex b/docs/logic.tex
index 51b4d0290..ecebd3f4b 100644
--- a/docs/logic.tex
+++ b/docs/logic.tex
@@ -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$):
\begin{align*}
- \type ::={}&
+ \type \bnfdef{}&
\sigtype \mid
1 \mid
\type \times \type \mid
\type \to \type
\\[0.4em]
- \term, \prop, \pred ::={}&
+ \term, \prop, \pred \bnfdef{}&
\var \mid
\sigfn(\term_1, \dots, \term_n) \mid
() \mid
--
GitLab