Commit 24d759e5 authored by Robbert Krebbers's avatar Robbert Krebbers

docs: Units no longer have to be discrete.

parent 2a745a85
Pipeline #2804 passed with stage
in 9 minutes and 20 seconds
......@@ -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}
......
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