From 24d759e58a01a6b29d7f2b9a8dfa1c312062b3ec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 10 Oct 2016 15:53:58 +0200
Subject: [PATCH] docs: Units no longer have to be discrete.
---
docs/algebra.tex | 1 -
1 file changed, 1 deletion(-)
diff --git a/docs/algebra.tex b/docs/algebra.tex
index e9b3208e4..e56383823 100644
--- a/docs/algebra.tex
+++ b/docs/algebra.tex
@@ -168,7 +168,6 @@ This operation is needed to prove that $\later$ commutes with separating conjunc
\item $\munit$ is valid: \\ $\All n. \munit \in \mval_n$
\item $\munit$ is a left-identity of the operation: \\
$\All \melt \in M. \munit \mtimes \melt = \melt$
- \item $\munit$ is a discrete COFE element
\item $\munit$ is its own core: \\ $\mcore\munit = \munit$
\end{enumerate}
\end{defn}
--
GitLab