Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have been trying to collect some information at 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.
Jelle Herold kindly added a section learning Coq to Coq.
Yes, that was kind! Thank you, Jelle.
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.
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.
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?
Yes! The entry deserves to be expanded a little here and there by some expert. Think of all the kids that visit this page.
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.
Added a “Relation to Predicativity” subsection to ordinal analysis to compensate. I hope these changes are not too far off what you wanted.
Yes, thanks for doing this.
added pointer to:
1 to 15 of 15