Miscellaneous


Topic Replies Views Activity
About the Miscellaneous category
2 119 February 12, 2019
Would Coq benefit from docstrings?
8 112 May 27, 2020
Why dependent type theory?
52 506 May 14, 2020
What is the difference between SSReflect and Czar?
7 106 May 13, 2020
Are there any declarative proof languages for Coq?
1 51 May 6, 2020
[Coq Discourse] Code listings broken in mailing list mode
3 57 March 26, 2020
Is there a full documentation of Coq's grammar?
6 160 March 2, 2020
Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)
1 100 February 24, 2020
Re: Coq vs lean for classical analysis
2 122 February 24, 2020
List of statements for verifying ATPs
2 89 February 20, 2020
Suggestions for bachelor thesis
4 171 February 12, 2020
Any resources for those studying Software Foundations on their own?
software-foundations
6 196 February 7, 2020
Does proof of coq consistency need axiom of choice?
4 200 February 6, 2020
Proof on normalization of CIC and its consistency
5 336 January 30, 2020
Any formally verified open source libraries?
13 343 December 25, 2019
Why doesn't Coq have a theorem Type like HOL Light?
5 280 December 24, 2019
High assurance / high code complexity use of Coq
17 612 December 4, 2019
Why is Coq consistent? What is the intended semantics?
faq
22 977 September 27, 2019
What does « .v » stand for?
2 186 September 14, 2019
Should other languages than English be allowed on the Discourse forum?
47 1069 September 12, 2019
Maintainers of Coquille plugin for Vim - please check the pull requests
5 303 August 28, 2019
Why is η-reduction illegal?
cic
3 201 August 1, 2019
Is "induction" polysemic?
2 260 March 21, 2019
Is Coq able to prove the identity x = x for infinite precision real numbers?
12 604 March 12, 2019
Syntax highlighting on Discourse
4 159 March 4, 2019