Commit 532f6d0a authored by Ralf Jung's avatar Ralf Jung

docs: intro rule for box

parent e12e5401
Pipeline #2777 passed with stage
in 9 minutes and 20 seconds
...@@ -310,6 +310,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda ...@@ -310,6 +310,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{\always{\prop} \proves \always{\propB}} {\always{\prop} \proves \always{\propB}}
\and \and
\begin{array}[c]{rMcMl} \begin{array}[c]{rMcMl}
\TRUE &\proves& \always{\TRUE} \\
\always{\prop} &\proves& \prop \\ \always{\prop} &\proves& \prop \\
\always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\ \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
\always{\prop} \land \propB &\proves& \always{\prop} * \propB \always{\prop} \land \propB &\proves& \always{\prop} * \propB
......
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