From 47d81be1200419d75e595053c0057ae9d2d2ee43 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 28 Jul 2016 15:02:41 +0200
Subject: [PATCH] add a comment about the 'no core' element

---
 docs/constructions.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/constructions.tex b/docs/constructions.tex
index 26cb9746e..40571188f 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -159,6 +159,8 @@ All cases of composition go to $\bot$.
   \mcore{\exinj(x)} \eqdef{}& \mnocore &
   \mcore{\bot} \eqdef{}& \bot
 \end{align*}
+Remember that $\mnocore$ is the ``dummy'' element in $\maybe\monoid$ indicating (in this case) that $\exinj(x)$ has no core.
+
 The step-indexed equivalence is inductively defined as follows:
 \begin{mathpar}
   \infer{x \nequiv{n} y}{\exinj(x) \nequiv{n} \exinj(y)}
-- 
GitLab