Timeline for Main statement as theorem or corollary
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 17, 2018 at 0:49 | comment | added | Eric Towers | @Lasse : Yes, my test in parentheses recommends using the common idiom of technical theorem followed by gee-whiz corollary. | |
| Jan 17, 2018 at 0:47 | comment | added | Eric Towers | @Lasse : Knuth eventually backed away from literate programming, realizing the intersection of good programmers and good writers is effectively empty. (There's a Knuth quote to this effect which I am too lazy to find.) | |
| Jan 16, 2018 at 17:52 | comment | added | Lasse | Having said that, after one proofs something in a theorem prover, often one wants to write a paper. In this paper, you would like to follow the structure of the formal proof as precisely as possible, for easy of comparison. So in my opinion, this problem also transfers to a paper setting. But do I understand from the text in your parenthesis, that you advocate using a theorem for B and a corollary for A? | |
| Jan 16, 2018 at 17:50 | comment | added | Lasse | Not everyone agrees with you that mixing content and presentation is an anti-pattern. For example, Knuth specificly invented literate programming to mix content and presentation. Theorem provers like Coq consciously support literate programming, and therefore have styling options. | |
| Jan 16, 2018 at 3:32 | history | answered | Eric Towers | CC BY-SA 3.0 |