Commit 6451214e authored by Ralf Jung's avatar Ralf Jung
Browse files

docs: fix \box properties

parent fe66881e
...@@ -498,8 +498,8 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i ...@@ -498,8 +498,8 @@ A type $\type$ being \emph{inhabited} means that $ \proves \wtt{\term}{\type}$ i
{\always{\prop} \proves \prop} {\always{\prop} \proves \prop}
\and \and
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\always{(\prop * \propB)} &\proves& \always{(\prop \land \propB)} \\ \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
\always{\prop} * \propB &\proves& \always{\prop} \land \propB \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
\always{\later\prop} &\provesIff& \later\always{\prop} \\ \always{\later\prop} &\provesIff& \later\always{\prop} \\
\end{array} \end{array}
\and \and
......
Supports Markdown
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