This commit is contained in:
Wen Kokke 2018-12-02 23:56:26 +01:00
parent f4a78c0755
commit ac4b0db5a0

View file

@ -299,8 +299,8 @@ just a couple of lines.
Here is the definition of addition in Agda:
\begin{code}
_+_ :
zero + n = n
suc m + n = suc (m + n)
zero + n = n
suc m + n = suc (m + n)
\end{code}
Let's unpack this definition. Addition is an infix operator. It is
@ -431,8 +431,8 @@ Once we have defined addition, we can define multiplication
as repeated addition.
\begin{code}
_*_ :
zero * n = zero
(suc m) * n = n + (m * n)
zero * n = zero
suc m * n = n + (m * n)
\end{code}
Again, rewriting gives us two familiar equations.