search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.36k stars 307 forks source link

Add reference to Unicode section #957

Closed buggymcbugfix closed 8 months ago

buggymcbugfix commented 8 months ago

A little in-place reminder for those who already garbage collected the contents of the "Getting Started" chapter.

EDIT: I put it as part of the first exercise as that should be the first time the issue of inputting special characters arises for anyone working through the book.

buggymcbugfix commented 8 months ago

My bad, I just noticed that several paragraphs further down, there is the following explanation:

You may have noticed that ℕ and → don't appear on your keyboard. They are symbols in unicode. At the end of each chapter is a list of all unicode symbols introduced in the chapter, including instructions on how to type them in the Emacs text editor. Here type refers to typing with fingers as opposed to data types!

This is a good and more thorough explanation that what I have in this PR, but I daresay it is not well-placed. Could we move this explanation up, near the first exercise?

wenkokke commented 8 months ago

Moved to issue #958