hazelgrove/agda-popl17

make comments and notation consistent with paper

Closed this issue · 5 comments

e.g. "focus" -> "cursor" and so on (do a systematic review going through the supplement)

Also the left cursor isn't quite the matching arrow to the right, but you can only see it in some fonts.

what do you mean by going through the supplement? what sorts of inconsistencies have you noticed or are you worried about?

Not particularly worried about anything, just want to make sure the
terminology is consistent. Would be good to label rules with comments
giving the corresponding rule numbers too, though that can wait until we
have final rule numbers (I did this in the implementation.)

On Wed, Jul 20, 2016 at 6:39 PM Ian Voysey notifications@github.com wrote:

what do you mean by going through the supplement? what sorts of
inconsistencies have you noticed or are you worried about?


You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#19 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AARIPjklTatXiGEJ6wKwxx7NkPAO7DBIks5qXqOPgaJpZM4JHscq
.

alright. we can deal with that later as a spit-polish thing, so once i figure out this arrow thing i'll close the issue.

also, alternatively, we could label the rules in the appendix with the constructor names, ideally programmatically.

the asymmetric rendering of the arrows (as in screenshot) seems to be an artifact of my laptop.
screen shot 2016-07-20 at 19 09 30
so i'm going worry about this later, or maybe never.