added pointer to:
Add the connection between Coq and the acronym CoC.
]]>Yes, thanks for doing this.
]]>Added a “Relation to Predicativity” subsection to ordinal analysis to compensate. I hope these changes are not too far off what you wanted.
]]>Changed the parenthetical summary of the “Believing In-Consistency” reference. It now links to ordinal analysis instead of predicativity. They’re related, but O’Connor focuses on ordinal analysis.
]]>Yes! The entry deserves to be expanded a little here and there by some expert. Think of all the kids that visit this page.
]]>Re #8: I’m not sure what you think is missing that would make sense to put on this page: O’Connor already says that ordinal analysis techniques don’t currently handle Coq’s theory, and some may find this worrisome.
Wait you mean to put something like what I just wrote next to the link?
]]>beautified the formatting of this reference:
Russell O’Connor, Believing In-Consistency
(on issues of predicativity)
but this seems a little thin a pointer. Any expert who cares about whatever issue is meant to be pointed out here might want to expand just a bit.
]]>and also to
]]>added pointer to
Since one needs to have already some experience with the Coq software environment in order to know what to do (and to think) when stumbling across a page like https://github.com/andrejbauer/Homotopy/tree/master/OberwolfachTutorial, and since it never occured to me (!) that I need to click on the word “raw” in order to get a pdf-file, I have split the pointer to that tutorial off as a category: Reference-entry
Oberwolfach HoTT-Coq tutorial,
uploaded the pdf there, and added some directions.
]]>Yes, that was kind! Thank you, Jelle.
]]>Jelle Herold kindly added a section learning Coq to Coq.
]]>I have added to the References-section at Coq
a pointer to a web-interface that runs Coq;
a pointer to a tool that allows to display Coq proofs from static Coq-files without having to load everything into a Coq-system itself.
I have been trying to collect some information at Coq.
]]>