OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook
http://openlogicproject.org/
Creative Commons Attribution 4.0 International
1.07k stars 241 forks source link

Typos, corrections and additions #259

Closed feffemannen closed 3 years ago

feffemannen commented 3 years ago

Observe the comment on the definition of a Turing computable function. With current definition composing functions seems problematic, this would be an easy way out, but examples, etc need to changed accordingly.

rzach commented 3 years ago

Ok I think we're agreed? I'll merge all the commits except the ones about the definition of TMs and TM output, and the ones about the soundness proof for NJ. Then I'll add the proposed changes with credit to you to the IL sections and TM sections.

(May take me a couple of days; classes start here today. Also I haven't tried to selectively merge things from a pull request before so I hope I don' break anything!)

rzach commented 3 years ago

Ok I think if I've done this right then everything but the Turing machine stuff is now included. So I'll close this and fix the TM stuff when I get to issue #191 Thanks for all this!