Skip to content

Commit b478583

Browse files
cjauvinChristian Jauvinwenkokke
authored
Improve the interactivity of the section on holes in Naturals (plfa#1089)
As discussed in plfa#1088, I suggest this small change to improve the interactivity of the file on Naturals a bit, and hopefully remove the confusion that I at least had with it. As I explain in the text, the only price to pay is that we have to use `_+'_` (plus prime) instead of `_+_`, because it was already defined in the file. --------- Co-authored-by: Christian Jauvin <cjauvin@explorance.com> Co-authored-by: Wen Kokke <wenkokke@users.noreply.github.com>
1 parent 1824aed commit b478583

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/plfa/part1/Naturals.lagda.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -784,6 +784,10 @@ Agda is designed to be used with the Emacs text editor, and the two
784784
in combination provide features that help to create definitions
785785
and proofs interactively.
786786

787+
Let's consider how to define addition interactively. (If you want to
788+
follow along, use a name other than `_+_` to avoid conflict with the
789+
definition above.)
790+
787791
Begin by typing:
788792

789793
_+_ : ℕ → ℕ → ℕ

0 commit comments

Comments
 (0)