pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2025-01-23 06:46:11 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Consistency of notation for implication (closes #46)

Browse source
This commit is contained in:
Adam Chlipala 2020-05-11 11:50:09 -04:00
parent b214d2c78a
commit b8d0cefa6a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
frap_book.tex
View file

@ -3764,10 +3764,10 @@ We can also define natural comparison operators between assertions, overloading
\end{eqnarray*} \end{eqnarray*}
The core connectives satisfy a number of handy algebraic laws. The core connectives satisfy a number of handy algebraic laws.
Here is a sampling. Here is a sampling (where we note that the first one takes advantage of the overloading of implication $\Rightarrow$ in two different senses).
$$\infer{P * \lift{\phi} \Rightarrow Q}{ $$\infer{P * \lift{\phi} \Rightarrow Q}{
\phi \rightarrow (P \Rightarrow Q) \phi \Rightarrow (P \Rightarrow Q)
} }
\quad \infer{P \Rightarrow Q * \lift{\phi}}{ \quad \infer{P \Rightarrow Q * \lift{\phi}}{
\phi \phi