OpenLogicProject / OpenLogic

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

Fix a couple of ref typos in the incompleteness part #375

Closed beastaugh closed 2 months ago

rzach commented 3 months ago

The def: prefix is to identify the type of environment referenced. It's not consistent or enforced (defn: is more common). So it looks like we should keep this unless I'm missing something

beastaugh commented 2 months ago

I made this change to fix the following undefined reference warning that was popping up in the incompleteness material (see attached log file from the sample project, lines 2820–2821).

LaTeX Warning: Reference `inc:int:def:def:standard-model' on page 1 undefined o
n input line 42.
rzach commented 2 months ago

Ah! I don't know why it fixed that problem, but the real problem is that open-logic-sample didn't include the file that contains the definition that's being referenced (in incompleteness/introduction/definitions.tex). I've fixed that. Let me know if we can close this then.

beastaugh commented 2 months ago

Yes, that's fixed it. Thanks!