mirror of
https://github.com/achlipala/frap.git
synced 2024-11-28 07:16:20 +00:00
Update before lecturing on BasicSyntax
This commit is contained in:
parent
d1d44e55f6
commit
d3be001671
1 changed files with 2 additions and 2 deletions
|
@ -46,7 +46,7 @@ For more information, see the book's home page:
|
||||||
\mbox{}\vfill
|
\mbox{}\vfill
|
||||||
\begin{center}
|
\begin{center}
|
||||||
|
|
||||||
Copyright Adam Chlipala 2015-2017.
|
Copyright Adam Chlipala 2015-2021.
|
||||||
|
|
||||||
|
|
||||||
This work is licensed under a
|
This work is licensed under a
|
||||||
|
@ -407,7 +407,7 @@ The notations are suggestive, but in fact we have free reign in choosing the set
|
||||||
The formal theory is then as follows, where we consider as ``true'' only those equalities that follow from the axioms.
|
The formal theory is then as follows, where we consider as ``true'' only those equalities that follow from the axioms.
|
||||||
$$\begin{array}{rrcl}
|
$$\begin{array}{rrcl}
|
||||||
\textrm{Variables} & x &\in& \mathsf{Strings} \\
|
\textrm{Variables} & x &\in& \mathsf{Strings} \\
|
||||||
\textrm{Terms} & e &::=& x \mid e + e \mid e \times e \\
|
\textrm{Terms} & e &::=& 0 \mid 1 \mid x \mid e + e \mid e \times e \\
|
||||||
\textrm{Propositions} & \phi &::=& e = e
|
\textrm{Propositions} & \phi &::=& e = e
|
||||||
\end{array}$$
|
\end{array}$$
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue