Various typos in text - Githubissues

thehottgame / TheHoTTGame

Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT

125 stars 15 forks source link

Various typos in text #10

Closed russellmcc closed 2 years ago

russellmcc commented 2 years ago

Thanks so much for this fantastic resource! I've just begun but I've noticed various typos in the text. The text for the game doesn't seem to be checked in, so I'll list them as I see them here. Please let me know if this isn't a helpful activity.

Quest 0 ** <emacsCommands appears in various places unexpectedly - is this a typo for some sort of link syntax?
Quest 1 ** Try typing _∙_ or ? ∙ ? in the hole (input /.) and refining should have input \. (notice slash direction) - small thing but could be confusing to agda beginners like me :-)

Jlh18 commented 2 years ago

Fixed the typos, thank you! Yeah the first one is a link thing for reStructuredText (which I'm finding a bit annoying to use), I should probably make a yas-snippet for writing links in rst or something so I stop making typos. Speaking of yas-snippets I made all my snippets for unicode (to use in rst for example) start with /, so I get super confused with forward and backward slashes @ - @

By not 'checked in' do you mean not part of this repo? If so the repo for the website is here https://github.com/thehottgame/theHoTTGameGuide (I saw you PRed for a typo in the solutions so I assume that's your intention?)

russellmcc commented 2 years ago

Thank you! I'll mention future typos in PRs to that repo :-) Thanks again for this resource!